Basic

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Vector/Basic.lean

Statistics

Metric	Count
Definitions Vector, actionCLM, asSmoothManifold, basis, coordCLM, equivEuclid, equivPi, euclidCLE, indexEquiv, innerProductSpace, instAddCommGroup, instAddCommMonoid, instChartedSpace, instCoeFunForallSumFinOfNatNatReal, instInnerReal, instModuleReal, instNorm, isNormedAddCommGroup, isNormedSpace, spatialCLM, spatialPart, temporalCLM, tensorial, timeComponent	24
Theorems abs_component_le_norm, actionCLM_apply, actionCLM_injective, actionCLM_surjective, apply_add, apply_smul, apply_sub, apply_sum, basis_apply, basis_eq_map_tensor_basis, basis_inner, basis_repr_apply, contDiff_apply, continuous_of_apply, coordCLM_apply, coord_contDiff, coord_continuous, coord_differentiable, coord_differentiableAt, differentiable_apply, equivEuclid_apply, equivPi_apply, fderiv_apply, fderiv_coord, inner_basis, inner_eq_equivEuclid, instFiniteDimensionalReal, map_apply_eq_basis_mulVec, neg_apply, neg_smul, norm_eq_equivEuclid, smul_add, smul_basis, smul_eq_mulVec, smul_eq_sum, smul_neg, smul_sub, smul_zero, spatialCLM_apply_eq_spatialPart, spatialCLM_basis_sum_inl, spatialCLM_basis_sum_inr, spatialPart_apply_eq_toCoord, spatialPart_basis_sum_inl, spatialPart_basis_sum_inr, sum_basis_eq_zero_iff, sum_inl_inr_basis_eq_zero_iff, temporalCLM_apply_eq_timeComponent, temporalCLM_basis_sum_inl, temporalCLM_basis_sum_inr, tensor_basis_map_eq_basis_reindex, tensor_basis_repr_toTensor_apply, timeComponent_basis_sum_inl, timeComponent_basis_sum_inr, toTensor_basis_eq_tensor_basis, toTensor_symm_apply, toTensor_symm_basis, toTensor_symm_pure, zero_apply, eq_of_action_vector_eq	59
Total	83

Lorentz

Definitions

Name	Category	Theorems
Vector 📖	CompOp	270 math math: LorentzGroup.toVector_continuous, Vector.minkowskiProduct_basis_right, Vector.actionCLM_surjective, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, StandardModel.HiggsField.toVec_smooth, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Velocity.mem_iff, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential, SpaceTime.differentiable_vector, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Velocity.norm_spatialPart_le_timeComponent, Velocity.minkowskiProduct_continuous_fst, Vector.isLorentz_iff_comp_adjoint_eq_id, StandardModel.HiggsField.const_toHiggsVec_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Velocity.minkowskiProduct_self_eq_one, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.apply_im_smooth, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, Vector.spatialCLM_apply_eq_spatialPart, Vector.minkowskiProduct_toCoord, SpaceTime.deriv_eq, Vector.smul_zero, Velocity.norm_spatialPart_sq_eq, Vector.toTensor_basis_eq_tensor_basis, Vector.spatialPart_basis_sum_inl, Vector.isLorentz_iff, Velocity.ext_iff, Vector.apply_sub, Vector.temporalCLM_basis_sum_inr, Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Vector.sum_inl_inr_basis_eq_zero_iff, LorentzGroup.generalizedBoost_apply_expand, Vector.inner_basis, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, StandardModel.HiggsField.const_apply, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Vector.inner_eq_equivEuclid, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, Vector.apply_add, LorentzGroup.generalizedBoost_timeComponent_eq, Vector.spatialCLM_basis_sum_inr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, Vector.contDiff_apply, SpaceTime.timeSpaceBasis_eq_map_basis, Vector.minkowskiProductMap_add_fst, Vector.isLorentz_iff_basis, StandardModel.HiggsField.inner_zero_right, Vector.minkowskiProduct_self_le_timeComponent_sq, LorentzGroup.genBoostAux₁_toMatrix_apply, Vector.basis_inner, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, LorentzGroup.toVector_neg, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, LorentzGroup.toVelocity_continuous, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Vector.coord_continuous, Vector.timeComponent_basis_sum_inl, Vector.tensor_basis_repr_toTensor_apply, SpaceTime.contDiff_vector, SpaceTime.toTimeAndSpace_basis_inl', Vector.minkowskiProduct_map_eq_adjoint, Vector.boost_inr_other_eq, StandardModel.HiggsField.inner_add_left, Vector.sum_basis_eq_zero_iff, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.LorentzCurrentDensity.chargeDensity_zero, Vector.neg_smul, Vector.fderiv_coord, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, LorentzGroup.toVector_minkowskiProduct_self, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_basis_inr, Vector.timeLike_iff_norm_sq_pos, Vector.coord_contDiff, Vector.map_apply_eq_basis_mulVec, Vector.minkowskiProductMap_add_snd, LorentzGroup.genearlizedBoost_apply_basis, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, Vector.minkowskiProduct_basis_left, Vector.abs_component_le_norm, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Velocity.timeComponent_pos, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, StandardModel.HiggsField.inner_neg_right, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Vector.minkowskiProduct_eq_zero_forall_iff, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, Vector.map_minkowskiProduct_eq_self_forall_iff, Vector.apply_sum, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Vector.minkowskiProductMap_smul_snd, Vector.smul_eq_sum, Velocity.minkowskiProduct_continuous_snd, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Vector.spatialCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, Vector.minkowskiProduct_toCoord_minkowskiMatrix, Velocity.zero_timeComponent, Electromagnetism.LorentzCurrentDensity.currentDensity_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, StandardModel.HiggsField.inner_neg_left, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Velocity.timeComponent_nonneg, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, LorentzGroup.generalizedBoost_continuous_snd, Vector.coord_differentiable, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, Velocity.isPathConnected, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, Vector.map_minkowskiProduct_eq_adjoint, StandardModel.HiggsField.inner_add_right, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, SpaceTime.apply_fderiv_eq_distDeriv, Vector.timeComponent_basis_sum_inr, Vector.coordCLM_apply, StandardModel.HiggsField.normSq_expand, Vector.boost_time_eq, Vector.coord_differentiableAt, StandardModel.HiggsField.Potential.toFun_zero, Vector.lightLike_iff_norm_sq_zero, Vector.spaceLike_iff_norm_sq_neg, Vector.minkowskiProduct_self_eq_timeComponent_spatialPart, Vector.minkowskiProduct_invariant, Vector.smul_neg, Vector.apply_smul, Vector.temporalCLM_basis_sum_inl, LorentzGroup.generalizedBoost_continuous_fst, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Vector.equivEuclid_apply, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Vector.causalCharacter_invariant, Vector.norm_eq_equivEuclid, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.ElectromagneticPotential.isExtrema_iff_gradLagrangian, Vector.toTensor_symm_basis, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, StandardModel.HiggsField.apply_re_smooth, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, StandardModel.HiggsField.inner_eq_expand, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, StandardModel.HiggsField.inner_zero_left, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, Vector.minkowskiProductMap_smul_fst, Vector.actionCLM_injective, LorentzGroup.generalizedBoost_apply_snd, LorentzGroup.toVector_eq_basis_iff_timeComponent_eq_one, StandardModel.HiggsField.inner_expand_conj, Vector.equivPi_apply, Vector.toTensor_symm_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, Vector.smul_basis, Vector.zero_apply, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, StandardModel.HiggsField.const_normSq, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, Vector.minkowskiProduct_apply, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, LorentzGroup.genBoostAux₂_self, Vector.basis_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, Vector.continuous_of_apply, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, Electromagnetism.ElectromagneticPotential.harmonicWaveX_contDiff, LorentzGroup.toVector_mul, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, Vector.smul_sub, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, StandardModel.HiggsField.inner_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Vector.differentiable_apply, Vector.instFiniteDimensionalReal, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, Vector.causalCharacter_zero, Electromagnetism.ElectromagneticPotential.constantEB_isExtrema, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.generalizedBoost_apply_eq_toCoord, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Vector.minkowskiProduct_eq_timeComponent_spatialPart, Vector.neg_causalCharacter_eq_self, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, Vector.isLorentz_iff_toMatrix_mem_lorentzGroup, Electromagnetism.ElectromagneticPotential.lagrangian_add_const, Vector.smul_eq_mulVec, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Vector.self_mem_lightConeBoundary, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, LorentzGroup.toVector_rotation, Vector.minkowskiProduct_symm, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isExtrema, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, Electromagnetism.ElectromagneticPotential.kineticTerm_add_const, LorentzGroup.genBoostAux₂_apply_basis, Electromagnetism.ElectromagneticPotential.constantEB_smooth, Vector.neg_apply, Vector.actionCLM_apply, LorentzGroup.genBoostAux₁_apply_basis, Vector.boost_inr_self_eq, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, StandardModel.HiggsField.contDiff, Vector.basis_repr_apply, StandardModel.HiggsField.normSq_zero, Vector.spatialPart_basis_sum_inr, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Vector.toTensor_symm_pure, Vector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.timeSpaceBasis_apply_inr, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_components, Velocity.zero_le_minkowskiProduct, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Vector.temporalCLM_apply_eq_timeComponent, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, Vector.smul_add, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Vector.basis_eq_map_tensor_basis, Vector.boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, Velocity.timeComponent_abs

Lorentz.Vector

Definitions

Name	Category	Theorems
actionCLM 📖	CompOp	3 math math: actionCLM_surjective, actionCLM_injective, actionCLM_apply
asSmoothManifold 📖	CompOp	27 math math: StandardModel.HiggsField.toVec_smooth, StandardModel.HiggsField.const_toHiggsVec_apply, StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.apply_im_smooth, StandardModel.HiggsField.const_apply, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, StandardModel.HiggsField.inner_zero_right, StandardModel.HiggsField.inner_add_left, StandardModel.HiggsField.inner_neg_right, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, StandardModel.HiggsField.inner_neg_left, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, StandardModel.HiggsField.inner_add_right, StandardModel.HiggsField.normSq_expand, StandardModel.HiggsField.Potential.toFun_zero, StandardModel.HiggsField.apply_re_smooth, StandardModel.HiggsField.inner_eq_expand, StandardModel.HiggsField.inner_zero_left, StandardModel.HiggsField.inner_expand_conj, StandardModel.HiggsField.const_normSq, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, StandardModel.HiggsField.inner_apply, StandardModel.HiggsField.contDiff, StandardModel.HiggsField.normSq_zero
basis 📖	CompOp	86 math math: minkowskiProduct_basis_right, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, SpaceTime.deriv_eq, toTensor_basis_eq_tensor_basis, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength, spatialPart_basis_sum_inl, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, temporalCLM_basis_sum_inr, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum, sum_inl_inr_basis_eq_zero_iff, inner_basis, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, spatialCLM_basis_sum_inr, SpaceTime.timeSpaceBasis_eq_map_basis, isLorentz_iff_basis, LorentzGroup.genBoostAux₁_toMatrix_apply, basis_inner, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, timeComponent_basis_sum_inl, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, sum_basis_eq_zero_iff, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, SpaceTime.toTimeAndSpace_basis_inr, map_apply_eq_basis_mulVec, LorentzGroup.genearlizedBoost_apply_basis, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, minkowskiProduct_basis_left, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, spatialCLM_basis_sum_inl, SpaceTime.distDeriv_apply, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, SpaceTime.apply_fderiv_eq_distDeriv, timeComponent_basis_sum_inr, temporalCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, LorentzGroup.toVector_eq_basis_iff_timeComponent_eq_one, smul_basis, SpaceTime.deriv_apply_eq, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, basis_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, isLorentz_iff_toMatrix_mem_lorentzGroup, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, LorentzGroup.toVector_rotation, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, LorentzGroup.genBoostAux₂_apply_basis, LorentzGroup.genBoostAux₁_apply_basis, basis_repr_apply, spatialPart_basis_sum_inr, tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, SpaceTime.timeSpaceBasis_apply_inr, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, basis_eq_map_tensor_basis
coordCLM 📖	CompOp	2 math math: fderiv_coord, coordCLM_apply
equivEuclid 📖	CompOp	3 math math: inner_eq_equivEuclid, equivEuclid_apply, norm_eq_equivEuclid
equivPi 📖	CompOp	1 math math: equivPi_apply
euclidCLE 📖	CompOp	—
indexEquiv 📖	CompOp	7 math math: toTensor_basis_eq_tensor_basis, tensor_basis_repr_toTensor_apply, toTensor_symm_basis, toTensor_symm_apply, toTensor_symm_pure, tensor_basis_map_eq_basis_reindex, basis_eq_map_tensor_basis
innerProductSpace 📖	CompOp	31 math math: Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.ElectromagneticPotential.kineticTerm_hasVarGradientAt, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.toFieldStrength_differentiable, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_gradLagrangian, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component
instAddCommGroup 📖	CompOp	145 math math: minkowskiProduct_basis_right, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Lorentz.Velocity.mem_iff, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential, SpaceTime.differentiable_vector, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Lorentz.Velocity.minkowskiProduct_continuous_fst, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Lorentz.Velocity.minkowskiProduct_self_eq_one, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, minkowskiProduct_toCoord, SpaceTime.deriv_eq, smul_zero, isLorentz_iff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, sum_inl_inr_basis_eq_zero_iff, LorentzGroup.generalizedBoost_apply_expand, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, LorentzGroup.generalizedBoost_timeComponent_eq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, isLorentz_iff_basis, minkowskiProduct_self_le_timeComponent_sq, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, LorentzGroup.toVector_neg, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, minkowskiProduct_map_eq_adjoint, sum_basis_eq_zero_iff, Electromagnetism.ElectromagneticPotential.toFieldStrength_differentiable, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.LorentzCurrentDensity.chargeDensity_zero, neg_smul, fderiv_coord, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, LorentzGroup.toVector_minkowskiProduct_self, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, timeLike_iff_norm_sq_pos, LorentzGroup.genearlizedBoost_apply_basis, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, minkowskiProduct_basis_left, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, minkowskiProduct_eq_zero_forall_iff, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, map_minkowskiProduct_eq_self_forall_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Lorentz.Velocity.minkowskiProduct_continuous_snd, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, minkowskiProduct_toCoord_minkowskiMatrix, Electromagnetism.LorentzCurrentDensity.currentDensity_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, coord_differentiable, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, map_minkowskiProduct_eq_adjoint, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, coord_differentiableAt, lightLike_iff_norm_sq_zero, spaceLike_iff_norm_sq_neg, SpaceTime.det_timeSpaceBasisEquiv, minkowskiProduct_self_eq_timeComponent_spatialPart, minkowskiProduct_invariant, smul_neg, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.ElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_symm_fderiv, zero_apply, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, minkowskiProduct_apply, LorentzGroup.genBoostAux₂_self, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, differentiable_apply, instFiniteDimensionalReal, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, causalCharacter_zero, Electromagnetism.ElectromagneticPotential.constantEB_isExtrema, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.generalizedBoost_apply_eq_toCoord, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, minkowskiProduct_eq_timeComponent_spatialPart, neg_causalCharacter_eq_self, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, Electromagnetism.ElectromagneticPotential.lagrangian_add_const, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, minkowskiProduct_symm, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isExtrema, LorentzGroup.genBoostAux₂_apply_basis, neg_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, Lorentz.Velocity.zero_le_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix
instAddCommMonoid 📖	CompOp	286 math math: minkowskiProduct_basis_right, actionCLM_surjective, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Lorentz.Velocity.mem_iff, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Lorentz.Velocity.minkowskiProduct_continuous_fst, isLorentz_iff_comp_adjoint_eq_id, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Lorentz.Velocity.minkowskiProduct_self_eq_one, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', SpaceTime.distTimeSlice_symm_apply, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, SpaceTime.deriv_sum_inr, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, spatialCLM_apply_eq_spatialPart, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, minkowskiProduct_toCoord, SpaceTime.deriv_eq, smul_zero, toTensor_basis_eq_tensor_basis, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength, spatialPart_basis_sum_inl, isLorentz_iff, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, temporalCLM_basis_sum_inr, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, sum_inl_inr_basis_eq_zero_iff, LorentzGroup.generalizedBoost_apply_expand, inner_basis, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_fderiv, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, inner_eq_equivEuclid, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, apply_add, LorentzGroup.generalizedBoost_timeComponent_eq, spatialCLM_basis_sum_inr, SpaceTime.spaceTime_integral_eq_time_space_integral, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, SpaceTime.deriv_sum_inl, SpaceTime.timeSpaceBasis_eq_map_basis, minkowskiProductMap_add_fst, isLorentz_iff_basis, minkowskiProduct_self_le_timeComponent_sq, LorentzGroup.genBoostAux₁_toMatrix_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_add, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, basis_inner, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, timeComponent_basis_sum_inl, tensor_basis_repr_toTensor_apply, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, minkowskiProduct_map_eq_adjoint, boost_inr_other_eq, Electromagnetism.ElectromagneticPotential.gradKineticTerm_add, sum_basis_eq_zero_iff, Electromagnetism.ElectromagneticPotential.toFieldStrength_differentiable, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.ElectromagneticPotential.gradKineticTerm_smul, SpaceTime.time_val_toCoord_symm, neg_smul, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, LorentzGroup.toVector_minkowskiProduct_self, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_basis_inr, timeLike_iff_norm_sq_pos, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, map_apply_eq_basis_mulVec, minkowskiProductMap_add_snd, LorentzGroup.genearlizedBoost_apply_basis, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, minkowskiProduct_basis_left, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_smul, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.tensorDeriv_equivariant, minkowskiProduct_eq_zero_forall_iff, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, map_minkowskiProduct_eq_self_forall_iff, apply_sum, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, minkowskiProductMap_smul_snd, smul_eq_sum, Lorentz.Velocity.minkowskiProduct_continuous_snd, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, SpaceTime.deriv_equivariant, spatialCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, minkowskiProduct_toCoord_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, SpaceTime.coord_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, map_minkowskiProduct_eq_adjoint, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, SpaceTime.apply_fderiv_eq_distDeriv, SpaceTime.toTimeAndSpace_symm_apply_inr, timeComponent_basis_sum_inr, coordCLM_apply, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, boost_time_eq, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, lightLike_iff_norm_sq_zero, spaceLike_iff_norm_sq_neg, SpaceTime.det_timeSpaceBasisEquiv, minkowskiProduct_self_eq_timeComponent_spatialPart, minkowskiProduct_invariant, smul_neg, apply_smul, temporalCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, equivEuclid_apply, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, causalCharacter_invariant, Electromagnetism.ElectromagneticPotential.toFieldStrength_smul, norm_eq_equivEuclid, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, toTensor_symm_basis, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, minkowskiProductMap_smul_fst, actionCLM_injective, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, LorentzGroup.toVector_eq_basis_iff_timeComponent_eq_one, equivPi_apply, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, toTensor_symm_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_symm_fderiv, smul_basis, SpaceTime.deriv_apply_eq, SpaceTime.toTimeAndSpace_fderiv, SpaceTime.boost_x_smul, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, minkowskiProduct_apply, LorentzGroup.genBoostAux₂_self, basis_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, LorentzGroup.toVector_mul, smul_sub, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.generalizedBoost_apply_eq_toCoord, Electromagnetism.ElectromagneticPotential.kineticTerm_add_time_mul_const, SpaceTime.schwartzAction_apply, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Electromagnetism.ElectromagneticPotential.toFieldStrength_add, minkowskiProduct_eq_timeComponent_spatialPart, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, isLorentz_iff_toMatrix_mem_lorentzGroup, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.lagrangian_add_const, smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, LorentzGroup.toVector_rotation, minkowskiProduct_symm, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, Electromagnetism.ElectromagneticPotential.kineticTerm_add_const, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, LorentzGroup.genBoostAux₂_apply_basis, actionCLM_apply, LorentzGroup.genBoostAux₁_apply_basis, boost_inr_self_eq, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, basis_repr_apply, spatialPart_basis_sum_inr, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, toTensor_symm_pure, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.timeSpaceBasis_apply_inr, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Lorentz.Velocity.zero_le_minkowskiProduct, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component, temporalCLM_apply_eq_timeComponent, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, smul_add, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, basis_eq_map_tensor_basis, boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, SpaceTime.space_toCoord_symm, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
instChartedSpace 📖	CompOp	31 math math: StandardModel.HiggsField.toVec_smooth, StandardModel.HiggsField.normSq_smooth, StandardModel.HiggsField.const_toHiggsVec_apply, StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.inner_smooth, StandardModel.HiggsField.apply_im_smooth, StandardModel.HiggsField.const_apply, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, StandardModel.HiggsField.inner_zero_right, StandardModel.HiggsField.Potential.toFun_smooth, StandardModel.HiggsField.inner_add_left, StandardModel.HiggsField.inner_neg_right, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, StandardModel.HiggsField.inner_neg_left, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, StandardModel.HiggsField.inner_add_right, StandardModel.HiggsField.normSq_expand, StandardModel.HiggsField.Potential.toFun_zero, StandardModel.HiggsField.apply_re_smooth, StandardModel.HiggsField.inner_eq_expand, StandardModel.HiggsField.inner_zero_left, StandardModel.HiggsField.inner_expand_conj, StandardModel.HiggsField.toHiggsVec_smooth, StandardModel.HiggsField.const_normSq, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, StandardModel.HiggsField.inner_apply, StandardModel.HiggsField.contDiff, StandardModel.HiggsField.normSq_zero
instCoeFunForallSumFinOfNatNatReal 📖	CompOp	—
instInnerReal 📖	CompOp	3 math math: inner_basis, inner_eq_equivEuclid, basis_inner
instModuleReal 📖	CompOp	256 math math: minkowskiProduct_basis_right, actionCLM_surjective, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Lorentz.Velocity.mem_iff, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential, SpaceTime.differentiable_vector, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Lorentz.Velocity.minkowskiProduct_continuous_fst, isLorentz_iff_comp_adjoint_eq_id, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Lorentz.Velocity.minkowskiProduct_self_eq_one, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', SpaceTime.distTimeSlice_symm_apply, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, spatialCLM_apply_eq_spatialPart, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, minkowskiProduct_toCoord, SpaceTime.deriv_eq, smul_zero, toTensor_basis_eq_tensor_basis, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength, spatialPart_basis_sum_inl, isLorentz_iff, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, temporalCLM_basis_sum_inr, Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, sum_inl_inr_basis_eq_zero_iff, LorentzGroup.generalizedBoost_apply_expand, inner_basis, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, inner_eq_equivEuclid, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, LorentzGroup.generalizedBoost_timeComponent_eq, spatialCLM_basis_sum_inr, SpaceTime.spaceTime_integral_eq_time_space_integral, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, SpaceTime.timeSpaceBasis_eq_map_basis, isLorentz_iff_basis, minkowskiProduct_self_le_timeComponent_sq, LorentzGroup.genBoostAux₁_toMatrix_apply, basis_inner, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, timeComponent_basis_sum_inl, tensor_basis_repr_toTensor_apply, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, minkowskiProduct_map_eq_adjoint, boost_inr_other_eq, sum_basis_eq_zero_iff, Electromagnetism.ElectromagneticPotential.toFieldStrength_differentiable, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.ElectromagneticPotential.gradKineticTerm_smul, SpaceTime.time_val_toCoord_symm, neg_smul, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, fderiv_coord, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, LorentzGroup.toVector_minkowskiProduct_self, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_basis_inr, timeLike_iff_norm_sq_pos, map_apply_eq_basis_mulVec, LorentzGroup.genearlizedBoost_apply_basis, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, minkowskiProduct_basis_left, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, minkowskiProduct_eq_zero_forall_iff, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, map_minkowskiProduct_eq_self_forall_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, minkowskiProductMap_smul_snd, smul_eq_sum, Lorentz.Velocity.minkowskiProduct_continuous_snd, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, spatialCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, minkowskiProduct_toCoord_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, SpaceTime.coord_apply, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, coord_differentiable, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, map_minkowskiProduct_eq_adjoint, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, SpaceTime.apply_fderiv_eq_distDeriv, SpaceTime.toTimeAndSpace_symm_apply_inr, timeComponent_basis_sum_inr, coordCLM_apply, boost_time_eq, coord_differentiableAt, lightLike_iff_norm_sq_zero, spaceLike_iff_norm_sq_neg, SpaceTime.det_timeSpaceBasisEquiv, minkowskiProduct_self_eq_timeComponent_spatialPart, minkowskiProduct_invariant, smul_neg, apply_smul, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable, temporalCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, equivEuclid_apply, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, causalCharacter_invariant, norm_eq_equivEuclid, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, toTensor_symm_basis, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, minkowskiProductMap_smul_fst, actionCLM_injective, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, LorentzGroup.toVector_eq_basis_iff_timeComponent_eq_one, equivPi_apply, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, toTensor_symm_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_symm_fderiv, smul_basis, SpaceTime.toTimeAndSpace_fderiv, SpaceTime.boost_x_smul, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, minkowskiProduct_apply, LorentzGroup.genBoostAux₂_self, basis_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq, LorentzGroup.toVector_mul, smul_sub, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, differentiable_apply, instFiniteDimensionalReal, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.generalizedBoost_apply_eq_toCoord, SpaceTime.schwartzAction_apply, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, minkowskiProduct_eq_timeComponent_spatialPart, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, isLorentz_iff_toMatrix_mem_lorentzGroup, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.lagrangian_add_const, smul_eq_mulVec, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, LorentzGroup.toVector_rotation, minkowskiProduct_symm, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, LorentzGroup.genBoostAux₂_apply_basis, actionCLM_apply, LorentzGroup.genBoostAux₁_apply_basis, boost_inr_self_eq, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, basis_repr_apply, spatialPart_basis_sum_inr, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, toTensor_symm_pure, tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.timeSpaceBasis_apply_inr, SpaceTime.toTimeAndSpace_symm_apply_time_space, Lorentz.Velocity.zero_le_minkowskiProduct, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component, temporalCLM_apply_eq_timeComponent, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, smul_add, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, basis_eq_map_tensor_basis, boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, SpaceTime.space_toCoord_symm, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
instNorm 📖	CompOp	2 math math: abs_component_le_norm, norm_eq_equivEuclid
isNormedAddCommGroup 📖	CompOp	238 math math: LorentzGroup.toVector_continuous, minkowskiProduct_basis_right, actionCLM_surjective, LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, StandardModel.HiggsField.toVec_smooth, SpaceTime.distTimeSlice_distDeriv_inl, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Lorentz.Velocity.mem_iff, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, StandardModel.HiggsField.normSq_smooth, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential, SpaceTime.differentiable_vector, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Lorentz.Velocity.minkowskiProduct_continuous_fst, StandardModel.HiggsField.const_toHiggsVec_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Lorentz.Velocity.minkowskiProduct_self_eq_one, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', SpaceTime.distTimeSlice_symm_apply, StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.inner_smooth, StandardModel.HiggsField.apply_im_smooth, SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, SpaceTime.space_toTimeAndSpace_symm, SpaceTime.instIsAddHaarMeasureVolume, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, spatialCLM_apply_eq_spatialPart, minkowskiProduct_toCoord, SpaceTime.deriv_eq, isLorentz_iff, apply_sub, temporalCLM_basis_sum_inr, Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, sum_inl_inr_basis_eq_zero_iff, LorentzGroup.generalizedBoost_apply_expand, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distDeriv_comp_lorentz_action, StandardModel.HiggsField.const_apply, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, LorentzGroup.generalizedBoost_timeComponent_eq, spatialCLM_basis_sum_inr, SpaceTime.spaceTime_integral_eq_time_space_integral, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, contDiff_apply, SpaceTime.timeSpaceBasis_eq_map_basis, isLorentz_iff_basis, StandardModel.HiggsField.inner_zero_right, minkowskiProduct_self_le_timeComponent_sq, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, coord_continuous, StandardModel.HiggsField.Potential.toFun_smooth, SpaceTime.distDeriv_commute, SpaceTime.distTensorDeriv_equivariant, SpaceTime.contDiff_vector, SpaceTime.toTimeAndSpace_basis_inl', minkowskiProduct_map_eq_adjoint, StandardModel.HiggsField.inner_add_left, sum_basis_eq_zero_iff, SpaceTime.distTimeSlice_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, SpaceTime.instIsOpenPosMeasureVolume, fderiv_coord, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, LorentzGroup.toVector_minkowskiProduct_self, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_basis_inr, timeLike_iff_norm_sq_pos, coord_contDiff, LorentzGroup.genearlizedBoost_apply_basis, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, minkowskiProduct_basis_left, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, SpaceTime.time_toTimeAndSpace_symm, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, SpaceTime.distTimeSlice_distDeriv_inr, StandardModel.HiggsField.inner_neg_right, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution, minkowskiProduct_eq_zero_forall_iff, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, map_minkowskiProduct_eq_self_forall_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, minkowskiProductMap_smul_snd, Lorentz.Velocity.minkowskiProduct_continuous_snd, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, spatialCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, minkowskiProduct_toCoord_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, StandardModel.HiggsField.inner_neg_left, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, coord_differentiable, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, map_minkowskiProduct_eq_adjoint, StandardModel.HiggsField.inner_add_right, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, SpaceTime.apply_fderiv_eq_distDeriv, SpaceTime.toTimeAndSpace_symm_apply_inr, coordCLM_apply, StandardModel.HiggsField.normSq_expand, SpaceTime.instBorelSpace, coord_differentiableAt, StandardModel.HiggsField.Potential.toFun_zero, lightLike_iff_norm_sq_zero, spaceLike_iff_norm_sq_neg, SpaceTime.det_timeSpaceBasisEquiv, minkowskiProduct_self_eq_timeComponent_spatialPart, minkowskiProduct_invariant, apply_smul, temporalCLM_basis_sum_inl, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, StandardModel.HiggsField.apply_re_smooth, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, SpaceTime.timeSpaceBasis_addHaar, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, StandardModel.HiggsField.inner_eq_expand, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, StandardModel.HiggsField.inner_zero_left, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, minkowskiProductMap_smul_fst, actionCLM_injective, LorentzGroup.generalizedBoost_apply_snd, StandardModel.HiggsField.inner_expand_conj, equivPi_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_symm_fderiv, smul_basis, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const, StandardModel.HiggsField.toHiggsVec_smooth, SpaceTime.instIsFiniteMeasureOnCompactsVolume, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, StandardModel.HiggsField.const_normSq, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, SpaceTime.schwartzAction_surjective, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, minkowskiProduct_apply, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, continuous_of_apply, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, Electromagnetism.ElectromagneticPotential.harmonicWaveX_contDiff, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, smul_sub, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, StandardModel.HiggsField.inner_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, differentiable_apply, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, LorentzGroup.genBoostAux₂_toMatrix_apply, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, LorentzGroup.generalizedBoost_apply_eq_toCoord, SpaceTime.schwartzAction_apply, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, SpaceTime.distDeriv_inr_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, SpaceTime.schwartzAction_mul_apply, minkowskiProduct_eq_timeComponent_spatialPart, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.lagrangian_add_const, SpaceTime.distDeriv_inl_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, minkowskiProduct_symm, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, SpaceTime.lorentzGroup_smul_dist_apply, LorentzGroup.genBoostAux₂_apply_basis, Electromagnetism.ElectromagneticPotential.constantEB_smooth, actionCLM_apply, LorentzGroup.genBoostAux₁_apply_basis, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, StandardModel.HiggsField.contDiff, StandardModel.HiggsField.normSq_zero, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_components, Lorentz.Velocity.zero_le_minkowskiProduct, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, temporalCLM_apply_eq_timeComponent, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, SpaceTime.distTensorDeriv_apply, SpaceTime.space_toCoord_symm, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, SpaceTime.schwartzAction_injective
isNormedSpace 📖	CompOp	133 math math: StandardModel.HiggsField.toVec_smooth, SpaceTime.distTimeSlice_distDeriv_inl, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, StandardModel.HiggsField.normSq_smooth, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, StandardModel.HiggsField.const_toHiggsVec_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.distDeriv_apply', SpaceTime.distTimeSlice_symm_apply, StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.inner_smooth, StandardModel.HiggsField.apply_im_smooth, SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distDeriv_comp_lorentz_action, StandardModel.HiggsField.const_apply, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, contDiff_apply, StandardModel.HiggsField.inner_zero_right, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, StandardModel.HiggsField.Potential.toFun_smooth, SpaceTime.distDeriv_commute, SpaceTime.distTensorDeriv_equivariant, SpaceTime.contDiff_vector, StandardModel.HiggsField.inner_add_left, SpaceTime.distTimeSlice_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, coord_contDiff, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, SpaceTime.distTimeSlice_distDeriv_inr, StandardModel.HiggsField.inner_neg_right, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, StandardModel.HiggsField.inner_neg_left, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, StandardModel.HiggsField.inner_add_right, SpaceTime.apply_fderiv_eq_distDeriv, StandardModel.HiggsField.normSq_expand, StandardModel.HiggsField.Potential.toFun_zero, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Space.distOfFunction_vector_eval, StandardModel.HiggsField.apply_re_smooth, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, SpaceTime.timeSpaceBasis_addHaar, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, StandardModel.HiggsField.inner_eq_expand, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, StandardModel.HiggsField.inner_zero_left, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, StandardModel.HiggsField.inner_expand_conj, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, StandardModel.HiggsField.toHiggsVec_smooth, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, StandardModel.HiggsField.const_normSq, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, SpaceTime.schwartzAction_surjective, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, Electromagnetism.ElectromagneticPotential.harmonicWaveX_contDiff, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, StandardModel.HiggsField.inner_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, SpaceTime.schwartzAction_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, SpaceTime.schwartzAction_mul_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, SpaceTime.distDeriv_inl_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, SpaceTime.lorentzGroup_smul_dist_apply, Electromagnetism.ElectromagneticPotential.constantEB_smooth, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, StandardModel.HiggsField.contDiff, StandardModel.HiggsField.normSq_zero, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_components, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, SpaceTime.distTensorDeriv_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, SpaceTime.schwartzAction_injective
spatialCLM 📖	CompOp	3 math math: spatialCLM_apply_eq_spatialPart, spatialCLM_basis_sum_inr, spatialCLM_basis_sum_inl
spatialPart 📖	CompOp	13 math math: Lorentz.Velocity.norm_spatialPart_le_timeComponent, spatialCLM_apply_eq_spatialPart, Lorentz.Velocity.norm_spatialPart_sq_eq, spatialPart_basis_sum_inl, LorentzGroup.generalizedBoost_timeComponent_eq, timeLike_iff_time_lt_space, spatialPart_apply_eq_toCoord, minkowskiProduct_self_eq_timeComponent_spatialPart, timelike_time_dominates_space, timelike_spatial_lt_time_squared, minkowskiProduct_eq_timeComponent_spatialPart, spatialPart_basis_sum_inr, lightlike_eq_spatial_norm_of_eq_time
temporalCLM 📖	CompOp	3 math math: temporalCLM_basis_sum_inr, temporalCLM_basis_sum_inl, temporalCLM_apply_eq_timeComponent
tensorial 📖	CompOp	69 math math: Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, smul_zero, toTensor_basis_eq_tensor_basis, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, LorentzGroup.generalizedBoost_apply_expand, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.generalizedBoost_apply, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, tensor_basis_repr_toTensor_apply, boost_inr_other_eq, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, neg_smul, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, LorentzGroup.genearlizedBoost_apply_basis, SpaceTime.boost_zero_apply_time_space, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.tensorDeriv_equivariant, smul_eq_sum, SpaceTime.deriv_equivariant, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, boost_time_eq, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, minkowskiProduct_invariant, smul_neg, causalCharacter_invariant, toTensor_symm_basis, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, smul_basis, SpaceTime.boost_x_smul, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, LorentzGroup.toVector_mul, smul_sub, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, SpaceTime.schwartzAction_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, actionCLM_apply, boost_inr_self_eq, toTensor_symm_pure, tensor_basis_map_eq_basis_reindex, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, smul_add, basis_eq_map_tensor_basis, boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
timeComponent 📖	CompOp	20 math math: Lorentz.Velocity.mem_iff, LorentzGroup.not_isOrthochronous_iff_toVector_timeComponet_nonpos, Lorentz.Velocity.norm_spatialPart_le_timeComponent, LorentzGroup.generalizedBoost_timeComponent_eq, minkowskiProduct_self_le_timeComponent_sq, timeComponent_basis_sum_inl, LorentzGroup.toVector_timeComponent, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Lorentz.Velocity.timeComponent_pos, Lorentz.Velocity.zero_timeComponent, Lorentz.Velocity.timeComponent_nonneg, timeComponent_squared_pos_of_timelike, timeComponent_basis_sum_inr, minkowskiProduct_self_eq_timeComponent_spatialPart, timelike_time_dominates_space, timelike_spatial_lt_time_squared, minkowskiProduct_eq_timeComponent_spatialPart, LorentzGroup.isOrthochronous_iff_toVector_timeComponet_nonneg, temporalCLM_apply_eq_timeComponent, Lorentz.Velocity.timeComponent_abs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_component_le_norm 📖	mathematical	—	Lorentz.Vector instNorm	—	—
actionCLM_apply 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal actionCLM LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up tensorial	—	—
actionCLM_injective 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal actionCLM	—	—
actionCLM_surjective 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal actionCLM	—	—
apply_add 📖	mathematical	—	Lorentz.Vector instAddCommMonoid	—	—
apply_smul 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal	—	—
apply_sub 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup	—	—
apply_sum 📖	mathematical	—	Lorentz.Vector instAddCommMonoid	—	apply_add
basis_apply 📖	mathematical	—	Lorentz.Vector instAddCommMonoid instModuleReal basis	—	—
basis_eq_map_tensor_basis 📖	mathematical	—	basis TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector instAddCommMonoid instModuleReal TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis TensorSpecies.Tensorial.toTensor tensorial indexEquiv	—	toTensor_symm_basis
basis_inner 📖	mathematical	—	Lorentz.Vector instInnerReal instAddCommMonoid instModuleReal basis	—	basis_apply
basis_repr_apply 📖	mathematical	—	Lorentz.Vector instAddCommMonoid instModuleReal basis	—	—
contDiff_apply 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup isNormedSpace	—	—
continuous_of_apply 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup	—	—
coordCLM_apply 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal coordCLM	—	—
coord_contDiff 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup isNormedSpace	—	—
coord_continuous 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup	—	—
coord_differentiable 📖	mathematical	—	Lorentz.Vector instAddCommGroup instModuleReal isNormedAddCommGroup	—	—
coord_differentiableAt 📖	mathematical	—	Lorentz.Vector instAddCommGroup instModuleReal isNormedAddCommGroup	—	—
differentiable_apply 📖	mathematical	—	Lorentz.Vector instAddCommGroup instModuleReal isNormedAddCommGroup	—	—
equivEuclid_apply 📖	mathematical	—	Lorentz.Vector instAddCommMonoid instModuleReal equivEuclid	—	—
equivPi_apply 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal equivPi	—	—
fderiv_apply 📖	—	Lorentz.Vector instAddCommGroup instModuleReal isNormedAddCommGroup	—	—	—
fderiv_coord 📖	mathematical	—	Lorentz.Vector instAddCommGroup instModuleReal isNormedAddCommGroup coordCLM	—	—
inner_basis 📖	mathematical	—	Lorentz.Vector instInnerReal instAddCommMonoid instModuleReal basis	—	basis_apply
inner_eq_equivEuclid 📖	mathematical	—	Lorentz.Vector instInnerReal instAddCommMonoid instModuleReal equivEuclid	—	—
instFiniteDimensionalReal 📖	mathematical	—	Lorentz.Vector instAddCommGroup instModuleReal	—	—
map_apply_eq_basis_mulVec 📖	mathematical	—	Lorentz.Vector instAddCommMonoid instModuleReal basis	—	—
neg_apply 📖	mathematical	—	Lorentz.Vector instAddCommGroup	—	—
neg_smul 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial LorentzGroup.instNegElemMatrixSumFinOfNatNatReal instAddCommGroup	—	smul_eq_sum neg_apply
norm_eq_equivEuclid 📖	mathematical	—	Lorentz.Vector instNorm instAddCommMonoid instModuleReal equivEuclid	—	—
smul_add 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial	—	—
smul_basis 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial basis isNormedAddCommGroup	—	smul_eq_sum basis_apply
smul_eq_mulVec 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial	—	smul_eq_sum
smul_eq_sum 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial	—	TensorSpecies.Tensorial.smul_toTensor_symm TensorSpecies.Tensor.induction_on_pure TensorSpecies.Tensor.actionT_pure toTensor_symm_pure Lorentz.contrBasisFin_repr_apply Lorentz.ContrMod.mulVec_val TensorSpecies.Tensor.actionT_smul TensorSpecies.Tensor.actionT_add
smul_neg 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial instAddCommGroup	—	smul_eq_mulVec
smul_sub 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial isNormedAddCommGroup	—	smul_eq_mulVec
smul_zero 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial instAddCommGroup	—	smul_eq_mulVec
spatialCLM_apply_eq_spatialPart 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal spatialCLM spatialPart	—	—
spatialCLM_basis_sum_inl 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal spatialCLM basis	—	spatialPart_basis_sum_inl
spatialCLM_basis_sum_inr 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal spatialCLM basis	—	spatialCLM_apply_eq_spatialPart spatialPart_basis_sum_inr
spatialPart_apply_eq_toCoord 📖	mathematical	—	spatialPart	—	—
spatialPart_basis_sum_inl 📖	mathematical	—	spatialPart Lorentz.Vector instAddCommMonoid instModuleReal basis	—	basis_apply
spatialPart_basis_sum_inr 📖	mathematical	—	spatialPart Lorentz.Vector instAddCommMonoid instModuleReal basis	—	basis_apply
sum_basis_eq_zero_iff 📖	mathematical	—	Lorentz.Vector instAddCommMonoid isNormedAddCommGroup instModuleReal basis instAddCommGroup	—	—
sum_inl_inr_basis_eq_zero_iff 📖	mathematical	—	Lorentz.Vector instAddCommMonoid isNormedAddCommGroup instModuleReal basis instAddCommGroup	—	sum_basis_eq_zero_iff
temporalCLM_apply_eq_timeComponent 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal temporalCLM timeComponent	—	—
temporalCLM_basis_sum_inl 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal temporalCLM basis	—	basis_apply
temporalCLM_basis_sum_inr 📖	mathematical	—	Lorentz.Vector isNormedAddCommGroup instAddCommMonoid instModuleReal temporalCLM basis	—	basis_apply
tensor_basis_map_eq_basis_reindex 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up TensorSpecies.Tensor Lorentz.Vector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensor.basis TensorSpecies.Tensorial.toTensor tensorial basis indexEquiv	—	basis_eq_map_tensor_basis
tensor_basis_repr_toTensor_apply 📖	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 instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial indexEquiv	—	TensorSpecies.Tensor.induction_on_pure TensorSpecies.Tensor.basis_repr_pure toTensor_symm_pure
timeComponent_basis_sum_inl 📖	mathematical	—	timeComponent Lorentz.Vector instAddCommMonoid instModuleReal basis	—	basis_apply
timeComponent_basis_sum_inr 📖	mathematical	—	timeComponent Lorentz.Vector instAddCommMonoid instModuleReal basis	—	basis_apply
toTensor_basis_eq_tensor_basis 📖	mathematical	—	Lorentz.Vector TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instModuleReal TensorSpecies.Tensorial.toTensor tensorial basis TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis indexEquiv	—	toTensor_symm_basis
toTensor_symm_apply 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx indexEquiv TensorSpecies.repDim TensorSpecies.Tensor.basis	—	—
toTensor_symm_basis 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis indexEquiv basis	—	TensorSpecies.Tensor.basis_apply toTensor_symm_pure basis_apply
toTensor_symm_pure 📖	mathematical	—	TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F instAddCommMonoid instModuleReal TensorSpecies.Tensorial.toTensor tensorial TensorSpecies.Tensor.Pure.toTensor Lorentz.Contr Lorentz.contrBasisFin TensorSpecies.Tensor.ComponentIdx indexEquiv	—	toTensor_symm_apply TensorSpecies.Tensor.basis_repr_pure
zero_apply 📖	mathematical	—	Lorentz.Vector instAddCommGroup	—	—

LorentzGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_action_vector_eq 📖	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial	—	—	eq_of_mulVec_eq Lorentz.Vector.smul_eq_mulVec

---

← Back to Index