Basic

📁 Source: PhysLean/Relativity/LorentzGroup/Basic.lean

Statistics

Metric	Count
Definitions LorentzGroup, instInvertibleMatrixSumFinOfNatNatComplexCoeMonoidHomElemRealToComplex, instInvertibleMatrixSumFinOfNatNatRealValMemSet, instNegElemMatrixSumFinOfNatNatReal, lorentzGroup_notation, parity, toComplex, toGL, toProd, transpose, instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup, lorentzGroupIsGroup	12
Theorems coe_inv, coe_neg, comm_minkowskiMatrix, dual_mem, eq_of_mulVec_eq, instIsTopologicalGroupElemMatrixSumFinOfNatNatReal, inv_eq_dual, inv_neg, mem_iff_dual_mul_self, mem_iff_neg_mem, mem_iff_self_mul_dual, mem_iff_transpose, mem_iff_transpose_mul_minkowskiMatrix_mul_self, mem_mul, minkowskiMatrix_comm, mul_minkowskiMatrix_mul_transpose, one_mem, subtype_inv_mul, subtype_mul_inv, toComplex_inv, toComplex_mulVec_ofReal, toComplex_mul_minkowskiMatrix_mul_transpose, toComplex_transpose_mul_minkowskiMatrix_mul_self, toGL_embedding, toGL_injective, toProd_apply, toProd_continuous, toProd_embedding, toProd_eq_transpose_η, toProd_injective, transpose_inv, transpose_mul, transpose_mul_minkowskiMatrix_mul_self, transpose_one, transpose_val, lorentzGroupIsGroup_div, lorentzGroupIsGroup_mul_coe, lorentzGroupIsGroup_one_coe	38
Total	50

LorentzGroup

Definitions

Name	Category	Theorems
instInvertibleMatrixSumFinOfNatNatComplexCoeMonoidHomElemRealToComplex 📖	CompOp	—
instInvertibleMatrixSumFinOfNatNatRealValMemSet 📖	CompOp	—
instNegElemMatrixSumFinOfNatNatReal 📖	CompOp	6 math math: isOrthochronous_iff_not_neg, coe_neg, toVector_neg, Lorentz.Vector.neg_smul, inv_neg, neg_isOrthochronous_iff_not
lorentzGroup_notation 📖	CompOp	—
parity 📖	CompOp	2 math math: Lorentz.contrContrContractField.self_parity_eq_zero_iff, Lorentz.contrContrContractField.right_parity
toComplex 📖	CompOp	15 math math: Lorentz.contrContrToMatrix_ρ_symm, Lorentz.complexContrBasis_ρ_apply, Lorentz.coContrToMatrix_ρ, Lorentz.complexCoBasis_ρ_apply, Lorentz.coCoToMatrix_ρ, toComplex_inv, toComplex_mulVec_ofReal, Lorentz.coCoToMatrix_ρ_symm, Lorentz.contrCoToMatrix_ρ_symm, toComplex_mul_minkowskiMatrix_mul_transpose, Lorentz.contrCoToMatrix_ρ, Lorentz.complexContrBasis_ρ_val, Lorentz.coContrToMatrix_ρ_symm, toComplex_transpose_mul_minkowskiMatrix_mul_self, Lorentz.contrContrToMatrix_ρ
toGL 📖	CompOp	3 math math: toGL_injective, toProd_apply, toGL_embedding
toProd 📖	CompOp	5 math math: toProd_embedding, toProd_injective, toProd_apply, toProd_eq_transpose_η, toProd_continuous
transpose 📖	CompOp	10 math math: isOrthochronous_iff_transpose, Lorentz.CoVector.smul_eq_mulVec, boost_transpose_eq_self, transpose_inv, transpose_mul, minkowskiMatrix_comm, transpose_mem_rotations, transpose_one, comm_minkowskiMatrix, transpose_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inv 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup	—	mem_iff_dual_mul_self
coe_neg 📖	mathematical	—	LorentzGroup instNegElemMatrixSumFinOfNatNatReal	—	—
comm_minkowskiMatrix 📖	mathematical	—	LorentzGroup minkowskiMatrix transpose lorentzGroupIsGroup	—	mul_minkowskiMatrix_mul_transpose transpose_inv coe_inv transpose_val
dual_mem 📖	mathematical	LorentzGroup	minkowskiMatrix.dual	—	mem_iff_dual_mul_self minkowskiMatrix.dual_dual mem_iff_self_mul_dual
eq_of_mulVec_eq 📖	—	LorentzGroup	—	—	—
instIsTopologicalGroupElemMatrixSumFinOfNatNatReal 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup	—	toGL_embedding
inv_eq_dual 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup minkowskiMatrix.dual dual_mem	—	—
inv_neg 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup instNegElemMatrixSumFinOfNatNatReal	—	dual_mem inv_eq_dual
mem_iff_dual_mul_self 📖	mathematical	—	LorentzGroup minkowskiMatrix.dual	—	mem_iff_self_mul_dual
mem_iff_neg_mem 📖	mathematical	—	LorentzGroup	—	mem_iff_self_mul_dual
mem_iff_self_mul_dual 📖	mathematical	—	LorentzGroup minkowskiMatrix.dual	—	—
mem_iff_transpose 📖	mathematical	—	LorentzGroup	—	mem_iff_dual_mul_self mem_iff_self_mul_dual minkowskiMatrix.eq_transpose minkowskiMatrix.dual.eq_1
mem_iff_transpose_mul_minkowskiMatrix_mul_self 📖	mathematical	—	LorentzGroup minkowskiMatrix	—	mem_iff_dual_mul_self minkowskiMatrix.dual.eq_1 minkowskiMatrix.sq
mem_mul 📖	—	LorentzGroup	—	—	mem_iff_dual_mul_self minkowskiMatrix.dual_mul
minkowskiMatrix_comm 📖	mathematical	—	minkowskiMatrix LorentzGroup transpose lorentzGroupIsGroup	—	transpose_mul_minkowskiMatrix_mul_self transpose_inv coe_inv transpose_val subtype_inv_mul
mul_minkowskiMatrix_mul_transpose 📖	mathematical	—	LorentzGroup minkowskiMatrix	—	minkowskiMatrix.sq mem_iff_self_mul_dual
one_mem 📖	mathematical	—	LorentzGroup	—	mem_iff_dual_mul_self minkowskiMatrix.dual_id
subtype_inv_mul 📖	mathematical	—	LorentzGroup	—	—
subtype_mul_inv 📖	mathematical	—	LorentzGroup	—	—
toComplex_inv 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toComplex	—	—
toComplex_mulVec_ofReal 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toComplex	—	—
toComplex_mul_minkowskiMatrix_mul_transpose 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toComplex minkowskiMatrix	—	mul_minkowskiMatrix_mul_transpose
toComplex_transpose_mul_minkowskiMatrix_mul_self 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toComplex minkowskiMatrix	—	transpose_mul_minkowskiMatrix_mul_self
toGL_embedding 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup toGL	—	toProd_embedding toGL_injective
toGL_injective 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toGL	—	—
toProd_apply 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toProd toGL	—	—
toProd_continuous 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup toProd	—	—
toProd_embedding 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup toProd	—	toProd_continuous toProd_injective
toProd_eq_transpose_η 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toProd minkowskiMatrix.dual	—	—
toProd_injective 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup toProd	—	toProd_eq_transpose_η
transpose_inv 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup transpose	—	transpose_val coe_inv
transpose_mul 📖	mathematical	—	transpose LorentzGroup lorentzGroupIsGroup	—	—
transpose_mul_minkowskiMatrix_mul_self 📖	mathematical	—	LorentzGroup minkowskiMatrix	—	mem_iff_dual_mul_self minkowskiMatrix.sq
transpose_one 📖	mathematical	—	transpose LorentzGroup lorentzGroupIsGroup	—	—
transpose_val 📖	mathematical	—	LorentzGroup transpose	—	—

(root)

Definitions

Name	Category	Theorems
LorentzGroup 📖	CompOp	326 math math: Lorentz.CoVector.smul_eq_sum, LorentzGroup.toVector_continuous, realLorentzTensor.prodT_toComplex, Lorentz.contrContrContractField.ge_abs_inner_product, realLorentzTensor.tau_colorToComplex, LorentzGroup.isOrthochronous_iff_not_neg, Lorentz.coContrToMatrixRe_symm_expand_tmul, LorentzGroup.boost_inr_self_inl_0, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Lorentz.contrContrContractField.matrix_eq_iff_eq_forall', LorentzGroup.coe_inv, Lorentz.contrContrToMatrix_ρ_symm, Lorentz.CoVector.toTensor_symm_pure, LorentzGroup.orthchroMapReal_minus_one_or_one, LorentzGroup.id_joined_generalizedBoost, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, LorentzGroup.boost_inl_0_inr_other, Lorentz.coContrContract_apply_metric, Lorentz.coContrToMatrixRe_ρ_symm, LorentzGroup.IsOrthochronous.iff_in_orthchroRep_ker, LorentzGroup.mul_minkowskiMatrix_mul_transpose, LorentzGroup.toGL_injective, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Lorentz.contrContrContractField.inl_sq_eq, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Lorentz.contrContrContractField.matrix_eq_iff_eq_forall, lorentzGroupIsGroup_div, Lorentz.CoVector.smul_eq_mulVec, Lorentz.Contr.ρ_stdBasis, Lorentz.preContrCoUnit_apply_one, Lorentz.complexContrBasis_ρ_apply, realLorentzTensor.toComplex_injective, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, lorentzAlgebra.exp_isOrthochronous, lorentzAlgebra.exp_mem_restricted_lorentzGroup, LorentzGroup.mem_iff_transpose_mul_minkowskiMatrix_mul_self, SpaceTime.distTensorDeriv_toTensor_basis_repr, LorentzGroup.toVector_eq_fun, LorentzGroup.toProd_embedding, LorentzGroup.boost_zero_inr_0_inr_succ, LorentzGroup.boost_inr_other_inr, Lorentz.contrContrContractField.basis_left, Lorentz.coContrToMatrix_ρ, Lorentz.SL2CRep_ρ_basis, Lorentz.Vector.smul_zero, Lorentz.preCoMetricVal_expand_tmul, Lorentz.contrBasis_toFin1dℝ, Lorentz.Vector.toTensor_basis_eq_tensor_basis, LorentzGroup.restricted_normal_subgroup, LorentzGroup.boost_zero_eq_id, LorentzGroup.boost_zero_inr_nat_succ_inl_0, Lorentz.contr_preContrCoUnit, Lorentz.SL2C.toLorentzGroup_inl_inl, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, LorentzGroup.coe_neg, LorentzGroup.generalizedBoost_apply_expand, Lorentz.contrCoContract_tmul_symm, LorentzGroup.toVector_apply, LorentzGroup.isOrthochronous_inv_iff, LorentzGroup.mem_iff_self_mul_dual, LorentzGroup.orthchroMap_not_IsOrthochronous, SpaceTime.distDeriv_comp_lorentz_action, Lorentz.coCoToMatrixRe_symm_expand_tmul, Lorentz.inclCongrRealLorentz_ρ, lorentzGroupIsGroup_mul_coe, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, LorentzGroup.mem_rotations_iff, LorentzGroup.generalizedBoost_timeComponent_eq, Lorentz.preContrMetricVal_expand_tmul_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.isOrthochronous_of_restricted, LorentzGroup.generalizedBoost_apply, Lorentz.CoVector.smul_neg, LorentzGroup.boost_zero_inl_0_inr_succ, LorentzGroup.boost_inr_other_inl_0, realLorentzTensor.contrMetric_eq_fromPairT, LorentzGroup.toProd_injective, Lorentz.coContrToMatrixRe_ρ, LorentzGroup.toVector_neg, Lorentz.contrContrContractField.matrix_eq_id_iff, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, LorentzGroup.toVelocity_continuous, LorentzGroup.toProd_apply, Lorentz.contrCoContract_basis, Lorentz.Vector.tensor_basis_repr_toTensor_apply, SpaceTime.distTensorDeriv_equivariant, LorentzGroup.transpose_inv, Lorentz.contrContrContractField.dual_mulVec_right, Lorentz.Vector.boost_inr_other_eq, Lorentz.CoVector.basis_eq_map_tensor_basis, Lorentz.preCoContrUnitVal_expand_tmul, LorentzGroup.subtype_inv_mul, Lorentz.complexCoBasis_ρ_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, LorentzGroup.generalizedBoost_inv, Lorentz.continuous_contr, LorentzGroup.generalizedBoost_self, Lorentz.coCoToMatrix_ρ, Lorentz.Vector.neg_smul, realLorentzTensor.actionT_contrMetric, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, LorentzGroup.toVector_timeComponent, realLorentzTensor.coMetric_eq_fromConstPair, LorentzGroup.genearlizedBoost_apply_basis, LorentzGroup.det_of_joined, realLorentzTensor.repDim_eq_one_plus_dim, SpaceTime.boost_zero_apply_time_space, LorentzGroup.not_isOrthochronous_iff_le_neg_one, Lorentz.CoVector.smul_zero, Lorentz.contrContrContractField.self_parity_eq_zero_iff, lorentzGroupIsGroup_one_coe, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Lorentz.preCoMetric_apply_one, Lorentz.CoVector.smul_basis, LorentzGroup.mem_iff_neg_mem, realLorentzTensor.toComplex_eq_sum_basis, Lorentz.SL2C.toLorentzGroup_apply_coe, Lorentz.coCoToMatrixRe_ρ, Lorentz.ContrMod.rep_apply_toFin1dℝ, Lorentz.CoVector.actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, LorentzGroup.transpose_mul_minkowskiMatrix_mul_self, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution, SpaceTime.tensorDeriv_equivariant, Lorentz.contrContrContractField.on_basis, Lorentz.Vector.smul_eq_sum, Lorentz.preContrMetricVal_expand_tmul, LorentzGroup.inv_neg, Lorentz.contrBasisFin_repr_apply, realLorentzTensor.actionT_coMetric, SpaceTime.deriv_equivariant, Lorentz.coBasis_ρ_apply, realLorentzTensor.permT_toComplex, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, LorentzGroup.detRep_apply, Lorentz.contrBasis_ρ_apply, Lorentz.SL2C.toLorentzGroup_fst_col, LorentzGroup.boost_inr_inr_other, LorentzGroup.toGL_embedding, Lorentz.SL2C.toLorentzGroup_det_one, LorentzGroup.generalizedBoost_continuous_snd, Lorentz.contr_preCoContrUnit, lorentzAlgebra.exp_mem_lorentzGroup, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, LorentzGroup.boost.h, realLorentzTensor.evalT_toComplex, LorentzGroup.toComplex_inv, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, LorentzGroup.toRotation_continuous, Lorentz.SL2C.toLorentzGroup_isOrthochronous, LorentzGroup.transpose_mul, Lorentz.CoVector.toTensor_symm_basis, LorentzGroup.toComplex_mulVec_ofReal, Lorentz.Vector.boost_time_eq, Lorentz.coContrContract_hom_tmul, lorentzAlgebra.exp_isProper, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, LorentzGroup.ofSpecialOrthogonal_symm_continuous, LorentzGroup.mem_iff_transpose, LorentzGroup.minkowskiMatrix_comm, realLorentzTensor.repDim_up, Lorentz.coContrContract_basis, realLorentzTensor.repDim_down, LorentzGroup.boost_zero_inr_0_inr_nat_succ, Lorentz.SL2C.toSelfAdjointMap_pauliBasis, LorentzGroup.orthchroMap_IsOrthochronous, Lorentz.Vector.minkowskiProduct_invariant, Lorentz.Vector.smul_neg, LorentzGroup.mem_iff_invariant, LorentzGroup.generalizedBoost_continuous_fst, realLorentzTensor.contr_basis, Lorentz.contrContrContractField.le_inl_sq, Lorentz.SL2C.toRestrictedLorentzGroup_apply_coe_coe, realLorentzTensor.toComplex_equivariant, Lorentz.contrContrContractField.matrix_apply_stdBasis, Lorentz.Vector.causalCharacter_invariant, realLorentzTensor.toComplex_eq_zero_iff, Lorentz.preCoContrUnit_symm, Lorentz.Vector.toTensor_symm_basis, LorentzGroup.transpose_mem_rotations, Lorentz.coContrContract_tmul_symm, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Lorentz.contrContrContract_hom_tmul, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, LorentzGroup.boost_zero_inl_0_inr_nat_succ, LorentzGroup.boost_inr_other_inr_self, Lorentz.coCoToMatrix_ρ_symm, Lorentz.contrContrContractField.action_tmul, Lorentz.contrCoToMatrix_ρ_symm, realLorentzTensor.coMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, LorentzGroup.one_mem, Electromagnetism.DistElectromagneticPotential.isExterma_equivariant, LorentzGroup.detContinuous_eq_one, LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose, Lorentz.contrContrContractField.as_sum, 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, LorentzGroup.isOrthochronous_mul, LorentzGroup.boost_transpose_matrix_eq_self, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Lorentz.Vector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, Lorentz.coCoContract_hom_tmul, LorentzGroup.isOrthochronous_iff_ge_one, Lorentz.Vector.smul_basis, LorentzGroup.boost_zero_inr_succ_inr_0, LorentzGroup.ofSpecialOrthogonal_continuous, SpaceTime.boost_x_smul, LorentzGroup.boost_inr_self_inr_other, Lorentz.CoVector.smul_add, Lorentz.contrContrContractField.nondegenerate, LorentzGroup.inv_eq_dual, LorentzGroup.transpose_one, Lorentz.coCoToMatrixRe_ρ_symm, LorentzGroup.one_le_abs_timeComponent, Lorentz.SL2C.toMatrix_mem_lorentzGroup, LorentzGroup.comm_minkowskiMatrix, Lorentz.contrCoToMatrix_ρ, Lorentz.coBasisFin_repr_apply, Lorentz.SL2C.toLorentzGroup_eq_pauliBasis', SpaceTime.schwartzAction_surjective, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Lorentz.coBasisFin_toFin1dℝ, realLorentzTensor.τ_down_eq_up, Lorentz.contrContrToMatrixRe_symm_expand_tmul, realLorentzTensor.contrMetric_eq_fromConstPair, Lorentz.contrCoContract_hom_tmul, LorentzGroup.toVector_mul, Lorentz.Vector.smul_sub, LorentzGroup.isProper_iff, LorentzGroup.orthchroMapReal_on_not_IsOrthochronous, Lorentz.contrBasisFin_toFin1dℝ, Lorentz.SL2C.toSelfAdjointMap_basis, Lorentz.contrContrToMatrixRe_ρ_symm, Lorentz.contrContrContractField.right_parity, LorentzGroup.boost_zero_inr_succ_inl_0, Lorentz.contrContrContractField.ge_sub_norm, Lorentz.CoVector.toTensor_symm_apply, Lorentz.contrCoToMatrixRe_ρ, LorentzGroup.transpose_val, Lorentz.contrContrContractField.stdBasis_inl, LorentzGroup.generalizedBoost_in_connected_component_of_id, Lorentz.preContrCoUnitVal_expand_tmul, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, LorentzGroup.instIsTopologicalGroupElemMatrixSumFinOfNatNatReal, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, LorentzGroup.generalizedBoost_apply_eq_toCoord, Lorentz.contrCoToMatrixRe_symm_expand_tmul, Lorentz.contrContrContractField.as_sum_toSpace, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, SpaceTime.schwartzAction_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Lorentz.preCoContrUnit_apply_one, Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint, SpaceTime.schwartzAction_mul_apply, Lorentz.contrContrContractField.symm, LorentzGroup.generalizedBoost_mem_restricted, LorentzGroup.toProd_eq_transpose_η, Lorentz.complexContrBasis_ρ_val, Lorentz.Vector.isLorentz_iff_toMatrix_mem_lorentzGroup, realLorentzTensor.τ_up_eq_down, LorentzGroup.subtype_mul_inv, LorentzGroup.id_isOrthochronous, Lorentz.Vector.smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, LorentzGroup.boost_zero_inr_succ_inr_succ, Lorentz.contrContrContractField.matrix_apply_eq_iff_sub, LorentzGroup.isProper_mul, LorentzGroup.boost_inverse, Lorentz.contrContrContractField.on_basis_mulVec, LorentzGroup.orthchroRep_inv_eq_self, LorentzGroup.toProd_continuous, Lorentz.coContrToMatrix_ρ_symm, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, LorentzGroup.boost_inr_self_inr_self, Lorentz.preContrMetric_apply_one, Lorentz.coBasis_toFin1dℝ, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, LorentzGroup.toVector_rotation, Lorentz.preContrCoUnit_symm, Lorentz.contrCoToMatrixRe_ρ_symm, LorentzGroup.orthchroMapReal_on_IsOrthochronous, SpaceTime.lorentzGroup_smul_dist_apply, LorentzGroup.not_isOrthochronous_iff_le_zero, LorentzGroup.det_eq_one_or_neg_one, Lorentz.contrContrToMatrixRe_ρ, Lorentz.Vector.actionCLM_apply, LorentzGroup.detRep_continuous, Lorentz.Vector.boost_inr_self_eq, LorentzGroup.isProper_id, LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self, LorentzGroup.mem_iff_norm, Lorentz.Vector.toTensor_symm_pure, Lorentz.CoVector.smul_sub, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, LorentzGroup.isOrthochronous_mul_iff, LorentzGroup.detContinuous_eq_iff_det_eq, LorentzGroup.boost_inl_0_inl_0, Lorentz.contrCoContract_apply_metric, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, LorentzGroup.boost_inl_0_inr_self, LorentzGroup.boost_zero_inr_nat_succ_inr_0, Lorentz.contrContrContractField.dual_mulVec_left, LorentzGroup.detContinuous_eq_zero, Lorentz.contrContrToMatrix_ρ, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, Lorentz.Vector.smul_add, Lorentz.Vector.basis_eq_map_tensor_basis, Lorentz.preCoMetricVal_expand_tmul_minkowskiMatrix, Lorentz.Vector.boost_toCoord_eq, LorentzGroup.neg_isOrthochronous_iff_not, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, LorentzGroup.mem_iff_dual_mul_self, LorentzGroup.rotations_subset_restricted, SpaceTime.schwartzAction_injective
instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup 📖	CompOp	23 math math: LorentzGroup.toVector_continuous, LorentzGroup.orthchroMapReal_minus_one_or_one, LorentzGroup.id_joined_generalizedBoost, LorentzGroup.toProd_embedding, LorentzGroup.orthchroMap_not_IsOrthochronous, LorentzGroup.toVelocity_continuous, LorentzGroup.detRep_apply, LorentzGroup.toGL_embedding, LorentzGroup.generalizedBoost_continuous_snd, LorentzGroup.toRotation_continuous, LorentzGroup.ofSpecialOrthogonal_symm_continuous, LorentzGroup.orthchroMap_IsOrthochronous, LorentzGroup.generalizedBoost_continuous_fst, LorentzGroup.detContinuous_eq_one, LorentzGroup.ofSpecialOrthogonal_continuous, LorentzGroup.orthchroMapReal_on_not_IsOrthochronous, LorentzGroup.generalizedBoost_in_connected_component_of_id, LorentzGroup.instIsTopologicalGroupElemMatrixSumFinOfNatNatReal, LorentzGroup.toProd_continuous, LorentzGroup.orthchroMapReal_on_IsOrthochronous, LorentzGroup.detRep_continuous, LorentzGroup.detContinuous_eq_iff_det_eq, LorentzGroup.detContinuous_eq_zero
lorentzGroupIsGroup 📖	CompOp	260 math math: Lorentz.CoVector.smul_eq_sum, realLorentzTensor.prodT_toComplex, Lorentz.contrContrContractField.ge_abs_inner_product, realLorentzTensor.tau_colorToComplex, Lorentz.coContrToMatrixRe_symm_expand_tmul, Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric, Lorentz.contrContrContractField.matrix_eq_iff_eq_forall', LorentzGroup.coe_inv, Lorentz.contrContrToMatrix_ρ_symm, Lorentz.CoVector.toTensor_symm_pure, LorentzGroup.id_joined_generalizedBoost, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_tensor_basis_eq_basis, Lorentz.coContrContract_apply_metric, Lorentz.coContrToMatrixRe_ρ_symm, LorentzGroup.IsOrthochronous.iff_in_orthchroRep_ker, LorentzGroup.toGL_injective, Lorentz.CoVector.tensor_basis_repr_toTensor_apply, Lorentz.contrContrContractField.inl_sq_eq, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr, Lorentz.contrContrContractField.matrix_eq_iff_eq_forall, lorentzGroupIsGroup_div, Lorentz.CoVector.smul_eq_mulVec, Lorentz.Contr.ρ_stdBasis, Lorentz.preContrCoUnit_apply_one, Lorentz.complexContrBasis_ρ_apply, realLorentzTensor.toComplex_injective, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, lorentzAlgebra.exp_mem_restricted_lorentzGroup, SpaceTime.distTensorDeriv_toTensor_basis_repr, LorentzGroup.toProd_embedding, Lorentz.contrContrContractField.basis_left, Lorentz.coContrToMatrix_ρ, Lorentz.SL2CRep_ρ_basis, Lorentz.Vector.smul_zero, Lorentz.preCoMetricVal_expand_tmul, Lorentz.contrBasis_toFin1dℝ, Lorentz.Vector.toTensor_basis_eq_tensor_basis, LorentzGroup.restricted_normal_subgroup, LorentzGroup.boost_zero_eq_id, Lorentz.contr_preContrCoUnit, Lorentz.SL2C.toLorentzGroup_inl_inl, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, SpaceTime.tensorDeriv_toTensor_basis_repr, LorentzGroup.generalizedBoost_apply_expand, Lorentz.contrCoContract_tmul_symm, LorentzGroup.isOrthochronous_inv_iff, SpaceTime.distDeriv_comp_lorentz_action, Lorentz.coCoToMatrixRe_symm_expand_tmul, Lorentz.inclCongrRealLorentz_ρ, lorentzGroupIsGroup_mul_coe, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix, LorentzGroup.mem_rotations_iff, Lorentz.preContrMetricVal_expand_tmul_minkowskiMatrix, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, LorentzGroup.isOrthochronous_of_restricted, LorentzGroup.generalizedBoost_apply, Lorentz.CoVector.smul_neg, realLorentzTensor.contrMetric_eq_fromPairT, LorentzGroup.toProd_injective, Lorentz.coContrToMatrixRe_ρ, Lorentz.contrContrContractField.matrix_eq_id_iff, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, LorentzGroup.toVelocity_continuous, LorentzGroup.toProd_apply, Lorentz.contrCoContract_basis, Lorentz.Vector.tensor_basis_repr_toTensor_apply, SpaceTime.distTensorDeriv_equivariant, LorentzGroup.transpose_inv, Lorentz.contrContrContractField.dual_mulVec_right, Lorentz.Vector.boost_inr_other_eq, Lorentz.CoVector.basis_eq_map_tensor_basis, Lorentz.preCoContrUnitVal_expand_tmul, Lorentz.complexCoBasis_ρ_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, LorentzGroup.generalizedBoost_inv, Lorentz.continuous_contr, LorentzGroup.generalizedBoost_self, Lorentz.coCoToMatrix_ρ, Lorentz.Vector.neg_smul, realLorentzTensor.actionT_contrMetric, Lorentz.CoVector.tensor_basis_map_eq_basis_reindex, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant, realLorentzTensor.coMetric_eq_fromConstPair, LorentzGroup.genearlizedBoost_apply_basis, realLorentzTensor.repDim_eq_one_plus_dim, SpaceTime.boost_zero_apply_time_space, Lorentz.CoVector.smul_zero, Lorentz.contrContrContractField.self_parity_eq_zero_iff, lorentzGroupIsGroup_one_coe, LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct, Lorentz.preCoMetric_apply_one, Lorentz.CoVector.smul_basis, realLorentzTensor.toComplex_eq_sum_basis, Lorentz.SL2C.toLorentzGroup_apply_coe, Lorentz.coCoToMatrixRe_ρ, Lorentz.ContrMod.rep_apply_toFin1dℝ, Lorentz.CoVector.actionCLM_apply, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff, SpaceTime.tensorDeriv_equivariant, Lorentz.contrContrContractField.on_basis, Lorentz.Vector.smul_eq_sum, Lorentz.preContrMetricVal_expand_tmul, LorentzGroup.inv_neg, Lorentz.contrBasisFin_repr_apply, realLorentzTensor.actionT_coMetric, SpaceTime.deriv_equivariant, Lorentz.coBasis_ρ_apply, realLorentzTensor.permT_toComplex, realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix, LorentzGroup.detRep_apply, Lorentz.contrBasis_ρ_apply, Lorentz.SL2C.toLorentzGroup_fst_col, LorentzGroup.toGL_embedding, Lorentz.SL2C.toLorentzGroup_det_one, Lorentz.contr_preCoContrUnit, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, realLorentzTensor.evalT_toComplex, LorentzGroup.toComplex_inv, LorentzGroup.toRotation_continuous, Lorentz.SL2C.toLorentzGroup_isOrthochronous, LorentzGroup.transpose_mul, Lorentz.CoVector.toTensor_symm_basis, LorentzGroup.toComplex_mulVec_ofReal, Lorentz.Vector.boost_time_eq, Lorentz.coContrContract_hom_tmul, SpaceTime.deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, LorentzGroup.ofSpecialOrthogonal_symm_continuous, LorentzGroup.minkowskiMatrix_comm, realLorentzTensor.repDim_up, Lorentz.coContrContract_basis, realLorentzTensor.repDim_down, Lorentz.SL2C.toSelfAdjointMap_pauliBasis, Lorentz.Vector.minkowskiProduct_invariant, Lorentz.Vector.smul_neg, LorentzGroup.mem_iff_invariant, realLorentzTensor.contr_basis, Lorentz.contrContrContractField.le_inl_sq, Lorentz.SL2C.toRestrictedLorentzGroup_apply_coe_coe, realLorentzTensor.toComplex_equivariant, Lorentz.contrContrContractField.matrix_apply_stdBasis, Lorentz.Vector.causalCharacter_invariant, realLorentzTensor.toComplex_eq_zero_iff, Lorentz.preCoContrUnit_symm, Lorentz.Vector.toTensor_symm_basis, LorentzGroup.transpose_mem_rotations, Lorentz.coContrContract_tmul_symm, Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis, Lorentz.contrContrContract_hom_tmul, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Lorentz.coCoToMatrix_ρ_symm, Lorentz.contrContrContractField.action_tmul, Lorentz.contrCoToMatrix_ρ_symm, LorentzGroup.detRep_on_connected_component, realLorentzTensor.coMetric_eq_fromPairT, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose, Lorentz.contrContrContractField.as_sum, LorentzGroup.generalizedBoost_apply_snd, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, LorentzGroup.isOrthochronous_mul, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv, Lorentz.Vector.toTensor_symm_apply, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, Lorentz.coCoContract_hom_tmul, Lorentz.Vector.smul_basis, LorentzGroup.ofSpecialOrthogonal_continuous, SpaceTime.boost_x_smul, Lorentz.CoVector.smul_add, Lorentz.contrContrContractField.nondegenerate, LorentzGroup.inv_eq_dual, LorentzGroup.transpose_one, Lorentz.coCoToMatrixRe_ρ_symm, LorentzGroup.comm_minkowskiMatrix, Lorentz.contrCoToMatrix_ρ, Lorentz.coBasisFin_repr_apply, Lorentz.SL2C.toLorentzGroup_eq_pauliBasis', SpaceTime.schwartzAction_surjective, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, Lorentz.coBasisFin_toFin1dℝ, realLorentzTensor.τ_down_eq_up, Lorentz.contrContrToMatrixRe_symm_expand_tmul, realLorentzTensor.contrMetric_eq_fromConstPair, Lorentz.contrCoContract_hom_tmul, LorentzGroup.toVector_mul, Lorentz.Vector.smul_sub, LorentzGroup.isProper_iff, Lorentz.contrBasisFin_toFin1dℝ, Lorentz.SL2C.toSelfAdjointMap_basis, Lorentz.contrContrToMatrixRe_ρ_symm, Lorentz.contrContrContractField.right_parity, Lorentz.contrContrContractField.ge_sub_norm, Lorentz.CoVector.toTensor_symm_apply, Lorentz.contrCoToMatrixRe_ρ, Lorentz.contrContrContractField.stdBasis_inl, LorentzGroup.generalizedBoost_in_connected_component_of_id, Lorentz.preContrCoUnitVal_expand_tmul, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, LorentzGroup.instIsTopologicalGroupElemMatrixSumFinOfNatNatReal, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, Lorentz.contrCoToMatrixRe_symm_expand_tmul, Lorentz.contrContrContractField.as_sum_toSpace, Lorentz.CoVector.toTensor_basis_eq_tensor_basis, SpaceTime.schwartzAction_apply, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, Lorentz.preCoContrUnit_apply_one, Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint, SpaceTime.schwartzAction_mul_apply, Lorentz.contrContrContractField.symm, LorentzGroup.generalizedBoost_mem_restricted, LorentzGroup.toProd_eq_transpose_η, Lorentz.complexContrBasis_ρ_val, realLorentzTensor.τ_up_eq_down, LorentzGroup.id_isOrthochronous, Lorentz.Vector.smul_eq_mulVec, Electromagnetism.ElectromagneticPotential.deriv_equivariant, Lorentz.contrContrContractField.matrix_apply_eq_iff_sub, LorentzGroup.isProper_mul, LorentzGroup.boost_inverse, Lorentz.contrContrContractField.on_basis_mulVec, LorentzGroup.orthchroRep_inv_eq_self, LorentzGroup.toProd_continuous, Lorentz.coContrToMatrix_ρ_symm, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Lorentz.preContrMetric_apply_one, Lorentz.coBasis_toFin1dℝ, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, LorentzGroup.toVector_rotation, Lorentz.preContrCoUnit_symm, Lorentz.contrCoToMatrixRe_ρ_symm, SpaceTime.lorentzGroup_smul_dist_apply, Lorentz.contrContrToMatrixRe_ρ, Lorentz.Vector.actionCLM_apply, LorentzGroup.detRep_continuous, Lorentz.Vector.boost_inr_self_eq, LorentzGroup.isProper_id, LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self, LorentzGroup.mem_iff_norm, Lorentz.Vector.toTensor_symm_pure, Lorentz.CoVector.smul_sub, Lorentz.Vector.tensor_basis_map_eq_basis_reindex, LorentzGroup.isOrthochronous_mul_iff, Lorentz.contrCoContract_apply_metric, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant, Lorentz.contrContrContractField.dual_mulVec_left, Lorentz.contrContrToMatrix_ρ, Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant, Lorentz.Vector.smul_add, Lorentz.Vector.basis_eq_map_tensor_basis, Lorentz.preCoMetricVal_expand_tmul_minkowskiMatrix, Lorentz.Vector.boost_toCoord_eq, LorentzGroup.generalizedBoost_apply_fst, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, LorentzGroup.rotations_subset_restricted, SpaceTime.schwartzAction_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lorentzGroupIsGroup_div 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup LorentzGroup.one_mem minkowskiMatrix.dual	—	—
lorentzGroupIsGroup_mul_coe 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup	—	—
lorentzGroupIsGroup_one_coe 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup	—	—

---

← Back to Index