Contraction

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean

Statistics

Metric	Count
Definitions coCoContract, coContrContract, coModContrModBi, contrCoContract, contrContrContract, contrContrContractField, contrModCoModBi	7
Theorems coCoContract_hom_tmul, coContrContract_basis, coContrContract_hom_tmul, coContrContract_tmul_symm, contrCoContract_basis, contrCoContract_hom_tmul, contrCoContract_tmul_symm, action_tmul, as_sum, as_sum_toSpace, basis_left, dual_mulVec_left, dual_mulVec_right, ge_abs_inner_product, ge_sub_norm, inl_sq_eq, le_inl_sq, matrix_apply_eq_iff_sub, matrix_apply_stdBasis, matrix_eq_id_iff, matrix_eq_iff_eq_forall, matrix_eq_iff_eq_forall', nondegenerate, on_basis, on_basis_mulVec, right_parity, same_eq_det_toSelfAdjoint, self_parity_eq_zero_iff, stdBasis_inl, symm, contrContrContract_hom_tmul, mem_iff_invariant, mem_iff_norm	33
Total	40

Lorentz

Definitions

Name	Category	Theorems
coCoContract 📖	CompOp	1 math math: coCoContract_hom_tmul
coContrContract 📖	CompOp	6 math math: coContrContract_apply_metric, contr_preContrCoUnit, contrCoContract_tmul_symm, coContrContract_hom_tmul, coContrContract_basis, coContrContract_tmul_symm
coModContrModBi 📖	CompOp	—
contrCoContract 📖	CompOp	6 math math: contrCoContract_tmul_symm, contrCoContract_basis, contr_preCoContrUnit, coContrContract_tmul_symm, contrCoContract_hom_tmul, contrCoContract_apply_metric
contrContrContract 📖	CompOp	—
contrContrContractField 📖	CompOp	26 math math: contrContrContractField.ge_abs_inner_product, contrContrContractField.matrix_eq_iff_eq_forall', contrContrContractField.inl_sq_eq, contrContrContractField.matrix_eq_iff_eq_forall, contrContrContractField.basis_left, contrContrContractField.matrix_eq_id_iff, contrContrContractField.dual_mulVec_right, contrContrContractField.self_parity_eq_zero_iff, contrContrContractField.on_basis, LorentzGroup.mem_iff_invariant, contrContrContractField.le_inl_sq, contrContrContractField.matrix_apply_stdBasis, contrContrContract_hom_tmul, contrContrContractField.action_tmul, contrContrContractField.as_sum, contrContrContractField.nondegenerate, contrContrContractField.right_parity, contrContrContractField.ge_sub_norm, contrContrContractField.stdBasis_inl, contrContrContractField.as_sum_toSpace, contrContrContractField.same_eq_det_toSelfAdjoint, contrContrContractField.symm, contrContrContractField.matrix_apply_eq_iff_sub, contrContrContractField.on_basis_mulVec, LorentzGroup.mem_iff_norm, contrContrContractField.dual_mulVec_left
contrModCoModBi 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coCoContract_hom_tmul 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Co coCoContract CoMod.toFin1dℝ minkowskiMatrix	—	coContrContract_hom_tmul
coContrContract_basis 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Co Contr coContrContract coBasis contrBasis	—	coContrContract_hom_tmul coBasis_toFin1dℝ contrBasis_toFin1dℝ
coContrContract_hom_tmul 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Co Contr coContrContract CoMod.toFin1dℝ ContrMod.toFin1dℝ	—	—
coContrContract_tmul_symm 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Co Contr coContrContract contrCoContract	—	contrCoContract_tmul_symm
contrCoContract_basis 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Contr Co contrCoContract contrBasis coBasis	—	contrCoContract_hom_tmul contrBasis_toFin1dℝ coBasis_toFin1dℝ
contrCoContract_hom_tmul 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Contr Co contrCoContract ContrMod.toFin1dℝ CoMod.toFin1dℝ	—	—
contrCoContract_tmul_symm 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Contr Co contrCoContract coContrContract	—	contrCoContract_hom_tmul coContrContract_hom_tmul
contrContrContract_hom_tmul 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Contr contrContrContractField ContrMod.toFin1dℝ minkowskiMatrix	—	contrCoContract_hom_tmul

Lorentz.contrContrContractField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
action_tmul 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	—
as_sum 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.val	—	Lorentz.contrContrContract_hom_tmul
as_sum_toSpace 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.val Lorentz.ContrMod.toSpace	—	as_sum
basis_left 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.stdBasis minkowskiMatrix Lorentz.ContrMod.toFin1dℝ	—	as_sum Lorentz.ContrMod.stdBasis_apply_same Lorentz.ContrMod.stdBasis_inl_apply_inr Lorentz.ContrMod.stdBasis_apply
dual_mulVec_left 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec minkowskiMatrix.dual	—	symm dual_mulVec_right
dual_mulVec_right 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec minkowskiMatrix.dual	—	Lorentz.contrContrContract_hom_tmul Lorentz.ContrMod.mulVec_toFin1dℝ minkowskiMatrix.sq
ge_abs_inner_product 📖	mathematical	—	Lorentz.ContrMod.val Lorentz.ContrMod.toSpace LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	as_sum_toSpace
ge_sub_norm 📖	mathematical	—	Lorentz.ContrMod.val Lorentz.ContrMod.toSpace LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	ge_abs_inner_product
inl_sq_eq 📖	mathematical	—	Lorentz.ContrMod.val LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	as_sum
le_inl_sq 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.val	—	inl_sq_eq
matrix_apply_eq_iff_sub 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec	—	Lorentz.ContrMod.sub_mulVec
matrix_apply_stdBasis 📖	mathematical	—	minkowskiMatrix LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.stdBasis Lorentz.ContrMod.mulVec	—	on_basis_mulVec minkowskiMatrix.η_apply_mul_η_apply_diag
matrix_eq_id_iff 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec	—	matrix_eq_iff_eq_forall Lorentz.ContrMod.one_mulVec
matrix_eq_iff_eq_forall 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec	—	matrix_eq_iff_eq_forall'
matrix_eq_iff_eq_forall' 📖	mathematical	—	Lorentz.ContrMod.mulVec LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	Lorentz.ContrMod.sub_mulVec nondegenerate
nondegenerate 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	self_parity_eq_zero_iff symm
on_basis 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.stdBasis minkowskiMatrix	—	Lorentz.ContrMod.one_mulVec on_basis_mulVec minkowskiMatrix.off_diag_zero
on_basis_mulVec 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.stdBasis Lorentz.ContrMod.mulVec minkowskiMatrix	—	basis_left Lorentz.ContrMod.mulVec_toFin1dℝ Lorentz.ContrMod.toFin1dℝ_eq_val Lorentz.ContrMod.stdBasis_apply
right_parity 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField LorentzGroup.parity Lorentz.ContrMod.val	—	as_sum minkowskiMatrix.mulVec_inl_0 minkowskiMatrix.mulVec_inr_i
same_eq_det_toSelfAdjoint 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.toSelfAdjoint	—	Lorentz.ContrMod.toSelfAdjoint_apply_coe as_sum_toSpace PauliMatrix.pauliMatrix.eq_1 PauliMatrix.pauliMatrix.eq_2 PauliMatrix.pauliMatrix.eq_3 PauliMatrix.pauliMatrix.eq_4 Lorentz.ContrMod.toSpace.eq_1 Lorentz.ContrMod.toFin1dℝ_eq_val
self_parity_eq_zero_iff 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField LorentzGroup.parity	—	Lorentz.ContrMod.ext right_parity
stdBasis_inl 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod Lorentz.ContrMod.instAddCommMonoid Lorentz.ContrMod.instModuleReal Lorentz.ContrMod.stdBasis	—	as_sum Lorentz.ContrMod.stdBasis_apply_same Lorentz.ContrMod.stdBasis_inl_apply_inr
symm 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField	—	as_sum

LorentzGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff_invariant 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec	—	Lorentz.contrContrContractField.dual_mulVec_right Lorentz.ContrMod.mulVec_mulVec mem_iff_dual_mul_self Lorentz.ContrMod.one_mulVec Lorentz.contrContrContractField.matrix_eq_id_iff
mem_iff_norm 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup Lorentz.Contr Lorentz.contrContrContractField Lorentz.ContrMod.mulVec	—	mem_iff_invariant Lorentz.contrContrContractField.symm Lorentz.ContrMod.mulVec_add Lorentz.ContrMod.mulVec_sub

---

← Back to Index