FieldStrength

📁 Source: PhysLean/Electromagnetism/Kinematics/FieldStrength.lean

Statistics

Metric	Count
Definitions `fieldStrength`, `fieldStrengthAux`, `fieldStrengthMatrix`, `toFieldStrength`	4
Theorems `distDeriv_fieldStrength_diag_zero`, `fieldStrengthAux_basis_repr_apply`, `fieldStrengthAux_basis_repr_apply_eq_single`, `fieldStrengthAux_eq_add`, `fieldStrengthAux_eq_basis`, `fieldStrengthAux_tensor_basis_eq_basis`, `fieldStrength_antisymmetric_basis`, `fieldStrength_basis_repr_eq_single`, `fieldStrength_diag_zero`, `fieldStrength_eq_basis`, `fieldStrength_eq_fieldStrengthAux`, `fieldStrength_equivariant`, `toTensor_fieldStrengthAux`, `toTensor_fieldStrengthAux_basis_repr`, `fieldStrengthMatrix_add`, `fieldStrengthMatrix_antisymm`, `fieldStrengthMatrix_contDiff`, `fieldStrengthMatrix_diag_eq_zero`, `fieldStrengthMatrix_differentiable`, `fieldStrengthMatrix_differentiable_space`, `fieldStrengthMatrix_differentiable_time`, `fieldStrengthMatrix_eq`, `fieldStrengthMatrix_eq_tensor_basis_repr`, `fieldStrengthMatrix_equivariant`, `fieldStrengthMatrix_smooth`, `fieldStrengthMatrix_smul`, `toFieldStrength_add`, `toFieldStrength_antisymmetric`, `toFieldStrength_basis_repr_apply`, `toFieldStrength_basis_repr_apply_eq_single`, `toFieldStrength_differentiable`, `toFieldStrength_eq_add`, `toFieldStrength_eq_fieldStrengthMatrix`, `toFieldStrength_equivariant`, `toFieldStrength_smul`, `toFieldStrength_tensor_basis_eq_basis`, `toTensor_toFieldStrength`, `toTensor_toFieldStrength_basis_repr`	38
Total	42

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
`fieldStrength` 📖	CompOp	13 math math: `fieldStrength_antisymmetric_basis`, `distDeriv_fieldStrength_diag_zero`, `gradLagrangian_eq_tensor`, `gradKineticTerm_eq_distTensorDeriv`, `isExterma_iff_tensor`, `magneticFieldMatrix_basis_repr_eq_fieldStrength`, `fieldStrength_basis_repr_eq_single`, `fieldStrength_eq_basis`, `fieldStrength_eq_fieldStrengthAux`, `fieldStrength_diag_zero`, `electricField_eq_fieldStrength`, `fieldStrength_equivariant`, `gradKineticTerm_eq_fieldStrength`
`fieldStrengthAux` 📖	CompOp	8 math math: `fieldStrengthAux_tensor_basis_eq_basis`, `fieldStrengthAux_eq_add`, `fieldStrengthAux_basis_repr_apply`, `fieldStrengthAux_basis_repr_apply_eq_single`, `fieldStrength_eq_fieldStrengthAux`, `toTensor_fieldStrengthAux`, `fieldStrengthAux_eq_basis`, `toTensor_fieldStrengthAux_basis_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distDeriv_fieldStrength_diag_zero` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `SpaceTime.distDeriv` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength`	—	`SpaceTime.distDeriv_apply'` `fieldStrength_diag_zero`
`fieldStrengthAux_basis_repr_apply` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `fieldStrengthAux` `minkowskiMatrix` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.distDeriv`	—	`fieldStrengthAux_tensor_basis_eq_basis` `toTensor_fieldStrengthAux_basis_repr`
`fieldStrengthAux_basis_repr_apply_eq_single` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `fieldStrengthAux` `minkowskiMatrix` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.distDeriv`	—	`fieldStrengthAux_basis_repr_apply` `minkowskiMatrix.off_diag_zero`
`fieldStrengthAux_eq_add` 📖	mathematical	—	`fieldStrengthAux` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `TensorSpecies.Tensor` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `realLorentzTensor.Color.down` `TensorSpecies.Tensor.Pure.dropPairEmb` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.PermCond` `realLorentzTensor.instDecidableEqColor` `TensorSpecies.Tensor.contrT` `TensorSpecies.Tensor.contrT_decide` `TensorSpecies.τ` `TensorSpecies.Tensor.prodT` `TensorSpecies.Tensorial.self` `realLorentzTensor.contrMetric` `Lorentz.CoVector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.CoVector.tensorial` `Distribution` `SpaceTime` `Lorentz.CoVector.isNormedAddCommGroup` `Lorentz.CoVector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `deriv`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `fieldStrengthAux.eq_1` `TensorSpecies.Tensor.PermCond.comp` `TensorSpecies.Tensor.permT_permT`
`fieldStrengthAux_eq_basis` 📖	mathematical	—	`fieldStrengthAux` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `minkowskiMatrix` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.distDeriv` `Lorentz.Vector.basis`	—	`fieldStrengthAux_basis_repr_apply_eq_single`
`fieldStrengthAux_tensor_basis_eq_basis` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `fieldStrengthAux` `Lorentz.Vector.basis`	—	`TensorSpecies.Tensorial.basis_toTensor_apply` `TensorSpecies.Tensorial.basis_map_prod` `Lorentz.Vector.tensor_basis_map_eq_basis_reindex`
`fieldStrength_antisymmetric_basis` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength`	—	`fieldStrength_basis_repr_eq_single`
`fieldStrength_basis_repr_eq_single` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength` `minkowskiMatrix` `SpaceTime.distDeriv`	—	`fieldStrength.eq_1` `fieldStrengthAux_basis_repr_apply_eq_single`
`fieldStrength_diag_zero` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength`	—	`fieldStrength_basis_repr_eq_single`
`fieldStrength_eq_basis` 📖	mathematical	—	`Distribution` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength` `minkowskiMatrix` `SpaceTime.distDeriv` `Lorentz.Vector.basis`	—	`fieldStrength.eq_1` `fieldStrengthAux_eq_basis`
`fieldStrength_eq_fieldStrengthAux` 📖	mathematical	—	`Distribution` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `fieldStrength` `fieldStrengthAux`	—	—
`fieldStrength_equivariant` 📖	mathematical	—	`Electromagnetism.DistElectromagneticPotential` `Distribution` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.instAddCommGroup` `fieldStrength` `LorentzGroup` `SpaceTime.instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution` `realLorentzTensor.Color` `realLorentzTensor.Color.up` `Lorentz.Vector.tensorial` `TensorSpecies.Tensorial.prod` `lorentzGroupIsGroup` `realLorentzTensor`	—	`fieldStrength_eq_fieldStrengthAux` `SpaceTime.lorentzGroup_smul_dist_apply` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `fieldStrengthAux_eq_add` `deriv_equivariant` `realLorentzTensor.actionT_contrMetric` `TensorSpecies.Tensorial.toTensor_smul` `TensorSpecies.Tensor.prodT_equivariant` `TensorSpecies.Tensor.contrT_equivariant` `TensorSpecies.Tensor.permT_equivariant`
`toTensor_fieldStrengthAux` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensor` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `fieldStrengthAux` `realLorentzTensor.Color.down` `TensorSpecies.Tensor.Pure.dropPairEmb` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.PermCond` `realLorentzTensor.instDecidableEqColor` `TensorSpecies.Tensor.contrT` `TensorSpecies.Tensor.contrT_decide` `TensorSpecies.τ` `TensorSpecies.Tensor.prodT` `TensorSpecies.Tensorial.self` `realLorentzTensor.contrMetric` `Lorentz.CoVector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.CoVector.tensorial` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.CoVector.isNormedAddCommGroup` `Lorentz.CoVector.innerProductSpace` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.isNormedSpace` `Electromagnetism.DistElectromagneticPotential` `Lorentz.Vector.instAddCommGroup` `deriv`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `fieldStrengthAux_eq_add` `TensorSpecies.Tensorial.self_toTensor_apply`
`toTensor_fieldStrengthAux_basis_repr` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `fieldStrengthAux` `minkowskiMatrix` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.distDeriv`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `toTensor_fieldStrengthAux` `TensorSpecies.Tensorial.self_toTensor_apply` `TensorSpecies.Tensor.PermCond.inv_perserve_color` `TensorSpecies.Tensor.permT_basis_repr_symm_apply` `realLorentzTensor.repDim_eq_one_plus_dim` `realLorentzTensor.contrT_basis_repr_apply_eq_fin` `TensorSpecies.Tensor.prodT_basis_repr_apply` `realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix` `toTensor_deriv_basis_repr_apply`

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`fieldStrengthMatrix` 📖	CompOp	32 math math: `fieldStrengthMatrix_antisymm`, `toFieldStrength_eq_fieldStrengthMatrix`, `gradLagrangian_eq_sum_fieldStrengthMatrix`, `fieldStrengthMatrix_eq_tensor_basis_repr`, `fieldStrengthMatrix_inr_inl_eq_electricField`, `gradKineticTerm_eq_fieldStrength`, `fieldStrengthMatrix_add`, `fieldStrengthMatrix_eq_electric_magnetic`, `curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `fieldStrengthMatrix_diag_eq_zero`, `div_electricField_eq_fieldStrengthMatrix`, `magneticField_snd_eq_fieldStrengthMatrix`, `fieldStrengthMatrix_differentiable_space`, `fieldStrengthMatrix_equivariant`, `fieldStrengthMatrix_smul`, `canonicalMomentum_eq`, `magneticField_thd_eq_fieldStrengthMatrix`, `kineticTerm_eq_sum_fieldStrengthMatrix_sq`, `fieldStrengthMatrix_differentiable`, `fieldStrengthMatrix_smooth`, `fieldStrengthMatrix_differentiable_time`, `isExtrema_iff_fieldStrengthMatrix`, `magneticField_fst_eq_fieldStrengthMatrix`, `fieldStrengthMatrix_eq`, `electricField_eq_fieldStrengthMatrix`, `time_deriv_electricField_eq_fieldStrengthMatrix`, `kineticTerm_eq_sum_fieldStrengthMatrix`, `fieldStrengthMatrix_contDiff`, `fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime`, `magneticFieldMatrix_eq`, `fieldStrengthMatrix_inl_inr_eq_electricField`, `fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix`
`toFieldStrength` 📖	CompOp	18 math math: `toFieldStrength_antisymmetric`, `toFieldStrength_eq_fieldStrengthMatrix`, `fieldStrengthMatrix_eq_tensor_basis_repr`, `kineticTerm_eq_sum`, `gradLagrangian_eq_tensor`, `toFieldStrength_differentiable`, `toTensor_toFieldStrength`, `toTensor_toFieldStrength_basis_repr`, `toFieldStrength_smul`, `toFieldStrength_tensor_basis_eq_basis`, `isExtrema_iff_tensors`, `gradKineticTerm_eq_tensorDeriv`, `fieldStrengthMatrix_eq`, `toFieldStrength_basis_repr_apply_eq_single`, `toFieldStrength_eq_add`, `toFieldStrength_basis_repr_apply`, `toFieldStrength_add`, `toFieldStrength_equivariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fieldStrengthMatrix_add` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `Electromagnetism.ElectromagneticPotential` `Lorentz.Vector.instAddCommMonoid`	—	`fieldStrengthMatrix.eq_1` `toFieldStrength_add`
`fieldStrengthMatrix_antisymm` 📖	mathematical	—	`fieldStrengthMatrix`	—	`toFieldStrength_basis_repr_apply`
`fieldStrengthMatrix_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`fieldStrengthMatrix`	—	`toFieldStrength_basis_repr_apply_eq_single` `SpaceTime.deriv_eq` `SpaceTime.contDiff_vector`
`fieldStrengthMatrix_diag_eq_zero` 📖	mathematical	—	`fieldStrengthMatrix`	—	`toFieldStrength_basis_repr_apply_eq_single`
`fieldStrengthMatrix_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `fieldStrengthMatrix`	—	`SpaceTime.differentiable_vector` `toFieldStrength_basis_repr_apply_eq_single` `SpaceTime.deriv_eq`
`fieldStrengthMatrix_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `fieldStrengthMatrix` `Time` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`fieldStrengthMatrix_differentiable`
`fieldStrengthMatrix_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `fieldStrengthMatrix` `Space` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Space.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`fieldStrengthMatrix_differentiable`
`fieldStrengthMatrix_eq` 📖	mathematical	—	`fieldStrengthMatrix` `Lorentz.CoVector` `Lorentz.Vector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.Vector.instModuleReal` `Lorentz.CoVector.basis` `Lorentz.Vector.basis` `toFieldStrength`	—	—
`fieldStrengthMatrix_eq_tensor_basis_repr` 📖	mathematical	—	`fieldStrengthMatrix` `TensorSpecies.Tensor.ComponentIdx` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `toFieldStrength` `TensorSpecies.repDim`	—	`toFieldStrength_tensor_basis_eq_basis`
`fieldStrengthMatrix_equivariant` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `LorentzGroup` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.tensorial`	—	`fieldStrengthMatrix.eq_1` `toFieldStrength_equivariant` `TensorSpecies.Tensorial.smul_prod` `Lorentz.Vector.basis_repr_apply` `Lorentz.CoVector.basis_repr_apply` `Lorentz.Vector.smul_eq_sum`
`fieldStrengthMatrix_smooth` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`fieldStrengthMatrix`	—	`fieldStrengthMatrix_contDiff`
`fieldStrengthMatrix_smul` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `Electromagnetism.ElectromagneticPotential` `Lorentz.Vector.instAddCommMonoid`	—	`fieldStrengthMatrix.eq_1` `toFieldStrength_smul`
`toFieldStrength_add` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`toFieldStrength` `Electromagnetism.ElectromagneticPotential` `Lorentz.Vector.instAddCommMonoid`	—	`toFieldStrength_basis_repr_apply` `SpaceTime.deriv_eq`
`toFieldStrength_antisymmetric` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensor` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `toFieldStrength` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.PermCond` `realLorentzTensor.instDecidableEqColor`	—	`TensorSpecies.Tensor.PermCond.auto` `toTensor_toFieldStrength_basis_repr` `TensorSpecies.Tensor.PermCond.inv_perserve_color` `TensorSpecies.Tensor.permT_basis_repr_symm_apply`
`toFieldStrength_basis_repr_apply` 📖	mathematical	—	`Lorentz.CoVector` `Lorentz.Vector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.Vector.instModuleReal` `Lorentz.CoVector.basis` `Lorentz.Vector.basis` `toFieldStrength` `minkowskiMatrix` `SpaceTime.deriv` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.isNormedAddCommGroup`	—	`toFieldStrength_tensor_basis_eq_basis` `toTensor_toFieldStrength_basis_repr`
`toFieldStrength_basis_repr_apply_eq_single` 📖	mathematical	—	`Lorentz.CoVector` `Lorentz.Vector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.Vector.instModuleReal` `Lorentz.CoVector.basis` `Lorentz.Vector.basis` `toFieldStrength` `minkowskiMatrix` `SpaceTime.deriv` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.isNormedAddCommGroup`	—	`toFieldStrength_basis_repr_apply` `minkowskiMatrix.off_diag_zero`
`toFieldStrength_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.innerProductSpace` `toFieldStrength`	—	`toFieldStrength_eq_fieldStrengthMatrix` `fieldStrengthMatrix_differentiable`
`toFieldStrength_eq_add` 📖	mathematical	—	`toFieldStrength` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.innerProductSpace` `TensorSpecies.Tensor` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `realLorentzTensor.Color.down` `TensorSpecies.Tensor.Pure.dropPairEmb` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.PermCond` `realLorentzTensor.instDecidableEqColor` `TensorSpecies.Tensor.contrT` `TensorSpecies.Tensor.contrT_decide` `TensorSpecies.τ` `TensorSpecies.Tensor.prodT` `TensorSpecies.Tensorial.self` `realLorentzTensor.contrMetric` `Lorentz.CoVector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.CoVector.tensorial` `deriv`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `toFieldStrength.eq_1` `TensorSpecies.Tensor.PermCond.comp` `TensorSpecies.Tensor.permT_permT`
`toFieldStrength_eq_fieldStrengthMatrix` 📖	mathematical	—	`toFieldStrength` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `fieldStrengthMatrix` `Lorentz.Vector.basis`	—	—
`toFieldStrength_equivariant` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`toFieldStrength` `LorentzGroup` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.tensorial` `TensorSpecies.Tensorial.prod`	—	`toFieldStrength.eq_1` `deriv_equivariant` `realLorentzTensor.actionT_contrMetric` `TensorSpecies.Tensorial.toTensor_smul` `TensorSpecies.Tensor.prodT_equivariant` `TensorSpecies.Tensor.contrT_equivariant` `TensorSpecies.Tensor.permT_equivariant`
`toFieldStrength_smul` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`toFieldStrength` `Electromagnetism.ElectromagneticPotential` `Lorentz.Vector.instAddCommMonoid`	—	`toFieldStrength_basis_repr_apply` `SpaceTime.deriv_eq`
`toFieldStrength_tensor_basis_eq_basis` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `toFieldStrength` `Lorentz.Vector.basis`	—	`TensorSpecies.Tensorial.basis_toTensor_apply` `TensorSpecies.Tensorial.basis_map_prod` `Lorentz.Vector.tensor_basis_map_eq_basis_reindex`
`toTensor_toFieldStrength` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensor` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `toFieldStrength` `realLorentzTensor.Color.down` `TensorSpecies.Tensor.Pure.dropPairEmb` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.PermCond` `realLorentzTensor.instDecidableEqColor` `TensorSpecies.Tensor.contrT` `TensorSpecies.Tensor.contrT_decide` `TensorSpecies.τ` `TensorSpecies.Tensor.prodT` `TensorSpecies.Tensorial.self` `realLorentzTensor.contrMetric` `Lorentz.CoVector` `Lorentz.CoVector.instAddCommMonoid` `Lorentz.CoVector.instModuleReal` `Lorentz.CoVector.tensorial` `deriv`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `toFieldStrength_eq_add` `TensorSpecies.Tensorial.self_toTensor_apply`
`toTensor_toFieldStrength_basis_repr` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `realLorentzTensor.Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `TensorSpecies.Tensorial.toTensor` `TensorSpecies.Tensorial.prod` `Lorentz.Vector.tensorial` `toFieldStrength` `minkowskiMatrix` `SpaceTime.deriv` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.isNormedAddCommGroup`	—	`TensorSpecies.Tensor.PermCond.auto` `TensorSpecies.Tensor.contrT_decide` `toTensor_toFieldStrength` `TensorSpecies.Tensorial.self_toTensor_apply` `TensorSpecies.Tensor.PermCond.inv_perserve_color` `TensorSpecies.Tensor.permT_basis_repr_symm_apply` `realLorentzTensor.repDim_eq_one_plus_dim` `realLorentzTensor.contrT_basis_repr_apply_eq_fin` `TensorSpecies.Tensor.prodT_basis_repr_apply` `realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix` `toTensor_deriv_basis_repr_apply`

---

← Back to Index