Modules

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

Statistics

Metric	Count
Definitions `CoMod`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleReal`, `mulVec`, `rep`, `stdBasis`, `toFin1dℝ`, `toFin1dℝEquiv`, `toFin1dℝFun`, `val`, `ContrMod`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleReal`, `instTopologicalSpace`, `mulVec`, `norm`, `rep`, `stdBasis`, `toFin1dℝ`, `toFin1dℝEquiv`, `toFin1dℝFun`, `toSelfAdjoint`, `toSpace`, `val`, `«term_ᵥ__1»`, `«term_ᵥ_»`	28
Theorems `ext`, `ext_iff`, `mulVec_toFin1dℝ`, `mulVec_val`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_decomp`, `stdBasis_repr_apply_support_val`, `stdBasis_repr_apply_toFun`, `stdBasis_repr_symm_apply_val`, `stdBasis_toFin1dℝEquiv_apply_ne`, `stdBasis_toFin1dℝEquiv_apply_same`, `ext`, `ext_iff`, `mulVec_add`, `mulVec_mulVec`, `mulVec_sub`, `mulVec_toFin1dℝ`, `mulVec_val`, `one_mulVec`, `rep_apply_toFin1dℝ`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_decomp`, `stdBasis_inl_apply_inr`, `stdBasis_repr_apply_support_val`, `stdBasis_repr_apply_toFun`, `stdBasis_repr_symm_apply_val`, `stdBasis_toFin1dℝEquiv_apply_ne`, `stdBasis_toFin1dℝEquiv_apply_same`, `sub_mulVec`, `toFin1dℝEquiv_isInducing`, `toFin1dℝEquiv_symm_isInducing`, `toFin1dℝ_eq_val`, `toSelfAdjoint_apply`, `toSelfAdjoint_apply_coe`, `toSelfAdjoint_stdBasis`, `toSelfAdjoint_symm_basis`, `val_add`, `val_smul`	40
Total	68

Lorentz

Definitions

Name	Category	Theorems
`CoMod` 📖	CompData	8 math math: `CoMod.stdBasis_toFin1dℝEquiv_apply_same`, `CoMod.stdBasis_repr_apply_support_val`, `CoMod.stdBasis_apply`, `CoMod.stdBasis_apply_same`, `CoMod.stdBasis_decomp`, `CoMod.stdBasis_repr_apply_toFun`, `CoMod.stdBasis_repr_symm_apply_val`, `CoMod.stdBasis_toFin1dℝEquiv_apply_ne`
`ContrMod` 📖	CompData	32 math math: `ContrMod.toSelfAdjoint_apply_coe`, `ContrMod.stdBasis_apply_same`, `ContrMod.stdBasis_repr_symm_apply_val`, `Contr.ρ_stdBasis`, `contrContrContractField.basis_left`, `ContrMod.mulVec_add`, `ContrMod.stdBasis_inl_apply_inr`, `ContrMod.stdBasis_repr_apply_toFun`, `inclCongrRealLorentz_ρ`, `ContrMod.toFin1dℝEquiv_symm_isInducing`, `ContrMod.mulVec_sub`, `ContrMod.toSelfAdjoint_stdBasis`, `ContrMod.sub_mulVec`, `SL2C.toMatrix_apply_contrMod`, `ContrMod.stdBasis_decomp`, `ContrMod.val_add`, `ContrMod.rep_apply_toFin1dℝ`, `contrContrContractField.on_basis`, `ContrMod.stdBasis_toFin1dℝEquiv_apply_ne`, `ContrMod.toFin1dℝEquiv_isInducing`, `ContrMod.toSelfAdjoint_apply`, `ContrMod.stdBasis_repr_apply_support_val`, `contrContrContractField.matrix_apply_stdBasis`, `inclCongrRealLorentz_val`, `ContrMod.stdBasis_apply`, `contrContrContractField.stdBasis_inl`, `ContrMod.val_smul`, `contrContrContractField.same_eq_det_toSelfAdjoint`, `ContrMod.toSelfAdjoint_symm_basis`, `contrContrContractField.on_basis_mulVec`, `complexContrBasis_of_real`, `ContrMod.stdBasis_toFin1dℝEquiv_apply_same`
`«term_*ᵥ__1»` 📖	CompOp	—
`«term_*ᵥ_»` 📖	CompOp	—

Lorentz.CoMod

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	1 math math: `stdBasis_decomp`
`instAddCommMonoid` 📖	CompOp	8 math math: `stdBasis_toFin1dℝEquiv_apply_same`, `stdBasis_repr_apply_support_val`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_decomp`, `stdBasis_repr_apply_toFun`, `stdBasis_repr_symm_apply_val`, `stdBasis_toFin1dℝEquiv_apply_ne`
`instModuleReal` 📖	CompOp	8 math math: `stdBasis_toFin1dℝEquiv_apply_same`, `stdBasis_repr_apply_support_val`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_decomp`, `stdBasis_repr_apply_toFun`, `stdBasis_repr_symm_apply_val`, `stdBasis_toFin1dℝEquiv_apply_ne`
`mulVec` 📖	CompOp	2 math math: `mulVec_toFin1dℝ`, `mulVec_val`
`rep` 📖	CompOp	—
`stdBasis` 📖	CompOp	8 math math: `stdBasis_toFin1dℝEquiv_apply_same`, `stdBasis_repr_apply_support_val`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_decomp`, `stdBasis_repr_apply_toFun`, `stdBasis_repr_symm_apply_val`, `stdBasis_toFin1dℝEquiv_apply_ne`
`toFin1dℝ` 📖	CompOp	7 math math: `mulVec_toFin1dℝ`, `stdBasis_decomp`, `Lorentz.coContrContract_hom_tmul`, `Lorentz.coCoContract_hom_tmul`, `Lorentz.coBasisFin_toFin1dℝ`, `Lorentz.contrCoContract_hom_tmul`, `Lorentz.coBasis_toFin1dℝ`
`toFin1dℝEquiv` 📖	CompOp	4 math math: `stdBasis_toFin1dℝEquiv_apply_same`, `stdBasis_repr_apply_support_val`, `stdBasis_repr_apply_toFun`, `stdBasis_toFin1dℝEquiv_apply_ne`
`toFin1dℝFun` 📖	CompOp	—
`val` 📖	CompOp	6 math math: `ext_iff`, `stdBasis_apply`, `stdBasis_apply_same`, `stdBasis_repr_symm_apply_val`, `Lorentz.coBasisFin_repr_apply`, `mulVec_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`mulVec_toFin1dℝ` 📖	mathematical	—	`toFin1dℝ` `mulVec`	—	—
`mulVec_val` 📖	mathematical	—	`val` `mulVec`	—	—
`stdBasis_apply` 📖	mathematical	—	`val` `Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	—
`stdBasis_apply_same` 📖	mathematical	—	`val` `Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	`stdBasis_toFin1dℝEquiv_apply_same`
`stdBasis_decomp` 📖	mathematical	—	`Lorentz.CoMod` `instAddCommMonoid` `instAddCommGroup` `instModuleReal` `toFin1dℝ` `stdBasis`	—	`stdBasis_toFin1dℝEquiv_apply_ne` `stdBasis_toFin1dℝEquiv_apply_same`
`stdBasis_repr_apply_support_val` 📖	mathematical	—	`Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `stdBasis` `toFin1dℝEquiv`	—	—
`stdBasis_repr_apply_toFun` 📖	mathematical	—	`Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `stdBasis` `toFin1dℝEquiv`	—	—
`stdBasis_repr_symm_apply_val` 📖	mathematical	—	`val` `Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	—
`stdBasis_toFin1dℝEquiv_apply_ne` 📖	mathematical	—	`Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv` `stdBasis`	—	—
`stdBasis_toFin1dℝEquiv_apply_same` 📖	mathematical	—	`Lorentz.CoMod` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv` `stdBasis`	—	—

Lorentz.ContrMod

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	5 math math: `Lorentz.Contr.ρ_stdBasis`, `mulVec_sub`, `sub_mulVec`, `stdBasis_decomp`, `val_smul`
`instAddCommMonoid` 📖	CompOp	30 math math: `toSelfAdjoint_apply_coe`, `stdBasis_apply_same`, `stdBasis_repr_symm_apply_val`, `Lorentz.Contr.ρ_stdBasis`, `Lorentz.contrContrContractField.basis_left`, `mulVec_add`, `stdBasis_inl_apply_inr`, `stdBasis_repr_apply_toFun`, `Lorentz.inclCongrRealLorentz_ρ`, `toFin1dℝEquiv_symm_isInducing`, `toSelfAdjoint_stdBasis`, `Lorentz.SL2C.toMatrix_apply_contrMod`, `stdBasis_decomp`, `val_add`, `rep_apply_toFin1dℝ`, `Lorentz.contrContrContractField.on_basis`, `stdBasis_toFin1dℝEquiv_apply_ne`, `toFin1dℝEquiv_isInducing`, `toSelfAdjoint_apply`, `stdBasis_repr_apply_support_val`, `Lorentz.contrContrContractField.matrix_apply_stdBasis`, `Lorentz.inclCongrRealLorentz_val`, `stdBasis_apply`, `Lorentz.contrContrContractField.stdBasis_inl`, `val_smul`, `Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint`, `toSelfAdjoint_symm_basis`, `Lorentz.contrContrContractField.on_basis_mulVec`, `Lorentz.complexContrBasis_of_real`, `stdBasis_toFin1dℝEquiv_apply_same`
`instModuleReal` 📖	CompOp	28 math math: `toSelfAdjoint_apply_coe`, `stdBasis_apply_same`, `stdBasis_repr_symm_apply_val`, `Lorentz.Contr.ρ_stdBasis`, `Lorentz.contrContrContractField.basis_left`, `stdBasis_inl_apply_inr`, `stdBasis_repr_apply_toFun`, `Lorentz.inclCongrRealLorentz_ρ`, `toFin1dℝEquiv_symm_isInducing`, `toSelfAdjoint_stdBasis`, `Lorentz.SL2C.toMatrix_apply_contrMod`, `stdBasis_decomp`, `rep_apply_toFin1dℝ`, `Lorentz.contrContrContractField.on_basis`, `stdBasis_toFin1dℝEquiv_apply_ne`, `toFin1dℝEquiv_isInducing`, `toSelfAdjoint_apply`, `stdBasis_repr_apply_support_val`, `Lorentz.contrContrContractField.matrix_apply_stdBasis`, `Lorentz.inclCongrRealLorentz_val`, `stdBasis_apply`, `Lorentz.contrContrContractField.stdBasis_inl`, `val_smul`, `Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint`, `toSelfAdjoint_symm_basis`, `Lorentz.contrContrContractField.on_basis_mulVec`, `Lorentz.complexContrBasis_of_real`, `stdBasis_toFin1dℝEquiv_apply_same`
`instTopologicalSpace` 📖	CompOp	2 math math: `toFin1dℝEquiv_symm_isInducing`, `toFin1dℝEquiv_isInducing`
`mulVec` 📖	CompOp	18 math math: `Lorentz.contrContrContractField.matrix_eq_iff_eq_forall'`, `Lorentz.contrContrContractField.matrix_eq_iff_eq_forall`, `mulVec_add`, `mulVec_toFin1dℝ`, `mulVec_sub`, `Lorentz.contrContrContractField.matrix_eq_id_iff`, `Lorentz.contrContrContractField.dual_mulVec_right`, `sub_mulVec`, `Lorentz.SL2C.toMatrix_apply_contrMod`, `mulVec_mulVec`, `one_mulVec`, `LorentzGroup.mem_iff_invariant`, `Lorentz.contrContrContractField.matrix_apply_stdBasis`, `mulVec_val`, `Lorentz.contrContrContractField.matrix_apply_eq_iff_sub`, `Lorentz.contrContrContractField.on_basis_mulVec`, `LorentzGroup.mem_iff_norm`, `Lorentz.contrContrContractField.dual_mulVec_left`
`norm` 📖	CompOp	—
`rep` 📖	CompOp	1 math math: `rep_apply_toFin1dℝ`
`stdBasis` 📖	CompOp	18 math math: `stdBasis_apply_same`, `stdBasis_repr_symm_apply_val`, `Lorentz.Contr.ρ_stdBasis`, `Lorentz.contrContrContractField.basis_left`, `stdBasis_inl_apply_inr`, `stdBasis_repr_apply_toFun`, `toSelfAdjoint_stdBasis`, `stdBasis_decomp`, `Lorentz.contrContrContractField.on_basis`, `stdBasis_toFin1dℝEquiv_apply_ne`, `stdBasis_repr_apply_support_val`, `Lorentz.contrContrContractField.matrix_apply_stdBasis`, `stdBasis_apply`, `Lorentz.contrContrContractField.stdBasis_inl`, `toSelfAdjoint_symm_basis`, `Lorentz.contrContrContractField.on_basis_mulVec`, `Lorentz.complexContrBasis_of_real`, `stdBasis_toFin1dℝEquiv_apply_same`
`toFin1dℝ` 📖	CompOp	13 math math: `toSelfAdjoint_apply_coe`, `Lorentz.contrContrContractField.basis_left`, `Lorentz.contrBasis_toFin1dℝ`, `mulVec_toFin1dℝ`, `stdBasis_decomp`, `rep_apply_toFin1dℝ`, `toFin1dℝ_eq_val`, `toSelfAdjoint_apply`, `Lorentz.coContrContract_hom_tmul`, `Lorentz.contrContrContract_hom_tmul`, `Lorentz.inclCongrRealLorentz_val`, `Lorentz.contrCoContract_hom_tmul`, `Lorentz.contrBasisFin_toFin1dℝ`
`toFin1dℝEquiv` 📖	CompOp	6 math math: `stdBasis_repr_apply_toFun`, `toFin1dℝEquiv_symm_isInducing`, `stdBasis_toFin1dℝEquiv_apply_ne`, `toFin1dℝEquiv_isInducing`, `stdBasis_repr_apply_support_val`, `stdBasis_toFin1dℝEquiv_apply_same`
`toFin1dℝFun` 📖	CompOp	—
`toSelfAdjoint` 📖	CompOp	6 math math: `toSelfAdjoint_apply_coe`, `toSelfAdjoint_stdBasis`, `Lorentz.SL2C.toMatrix_apply_contrMod`, `toSelfAdjoint_apply`, `Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint`, `toSelfAdjoint_symm_basis`
`toSpace` 📖	CompOp	3 math math: `Lorentz.contrContrContractField.ge_abs_inner_product`, `Lorentz.contrContrContractField.ge_sub_norm`, `Lorentz.contrContrContractField.as_sum_toSpace`
`val` 📖	CompOp	17 math math: `Lorentz.contrContrContractField.ge_abs_inner_product`, `stdBasis_apply_same`, `Lorentz.contrContrContractField.inl_sq_eq`, `stdBasis_repr_symm_apply_val`, `stdBasis_inl_apply_inr`, `val_add`, `toFin1dℝ_eq_val`, `Lorentz.contrBasisFin_repr_apply`, `Lorentz.contrContrContractField.le_inl_sq`, `mulVec_val`, `Lorentz.contrContrContractField.as_sum`, `stdBasis_apply`, `Lorentz.contrContrContractField.right_parity`, `Lorentz.contrContrContractField.ge_sub_norm`, `val_smul`, `Lorentz.contrContrContractField.as_sum_toSpace`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`mulVec_add` 📖	mathematical	—	`mulVec` `Lorentz.ContrMod` `instAddCommMonoid`	—	—
`mulVec_mulVec` 📖	mathematical	—	`mulVec`	—	—
`mulVec_sub` 📖	mathematical	—	`mulVec` `Lorentz.ContrMod` `instAddCommGroup`	—	—
`mulVec_toFin1dℝ` 📖	mathematical	—	`toFin1dℝ` `mulVec`	—	—
`mulVec_val` 📖	mathematical	—	`val` `mulVec`	—	—
`one_mulVec` 📖	mathematical	—	`mulVec`	—	—
`rep_apply_toFin1dℝ` 📖	mathematical	—	`toFin1dℝ` `Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `LorentzGroup` `lorentzGroupIsGroup` `rep`	—	—
`stdBasis_apply` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	—
`stdBasis_apply_same` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	`stdBasis_toFin1dℝEquiv_apply_same`
`stdBasis_decomp` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instAddCommGroup` `instModuleReal` `toFin1dℝ` `stdBasis`	—	`stdBasis_toFin1dℝEquiv_apply_ne` `stdBasis_toFin1dℝEquiv_apply_same`
`stdBasis_inl_apply_inr` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	`stdBasis_toFin1dℝEquiv_apply_ne`
`stdBasis_repr_apply_support_val` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis` `toFin1dℝEquiv`	—	—
`stdBasis_repr_apply_toFun` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis` `toFin1dℝEquiv`	—	—
`stdBasis_repr_symm_apply_val` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `stdBasis`	—	—
`stdBasis_toFin1dℝEquiv_apply_ne` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv` `stdBasis`	—	—
`stdBasis_toFin1dℝEquiv_apply_same` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv` `stdBasis`	—	—
`sub_mulVec` 📖	mathematical	—	`mulVec` `Lorentz.ContrMod` `instAddCommGroup`	—	—
`toFin1dℝEquiv_isInducing` 📖	mathematical	—	`Lorentz.ContrMod` `instTopologicalSpace` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv`	—	—
`toFin1dℝEquiv_symm_isInducing` 📖	mathematical	—	`Lorentz.ContrMod` `instTopologicalSpace` `instAddCommMonoid` `instModuleReal` `toFin1dℝEquiv`	—	`toFin1dℝEquiv_isInducing`
`toFin1dℝ_eq_val` 📖	mathematical	—	`toFin1dℝ` `val`	—	—
`toSelfAdjoint_apply` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toSelfAdjoint` `toFin1dℝ` `PauliMatrix.pauliMatrix` `PauliMatrix.pauliMatrix_selfAdjoint`	—	`PauliMatrix.pauliMatrix_selfAdjoint` `PauliMatrix.pauliSelfAdjoint'_linearly_independent` `PauliMatrix.pauliSelfAdjoint'_span`
`toSelfAdjoint_apply_coe` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toSelfAdjoint` `toFin1dℝ` `PauliMatrix.pauliMatrix`	—	`PauliMatrix.pauliMatrix_selfAdjoint` `toSelfAdjoint_apply`
`toSelfAdjoint_stdBasis` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toSelfAdjoint` `stdBasis` `PauliMatrix.pauliBasis'`	—	`PauliMatrix.pauliMatrix_selfAdjoint` `toSelfAdjoint_apply` `PauliMatrix.pauliSelfAdjoint'_linearly_independent` `PauliMatrix.pauliSelfAdjoint'_span`
`toSelfAdjoint_symm_basis` 📖	mathematical	—	`Lorentz.ContrMod` `instAddCommMonoid` `instModuleReal` `toSelfAdjoint` `PauliMatrix.pauliBasis'` `stdBasis`	—	`toSelfAdjoint_stdBasis`
`val_add` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommMonoid`	—	—
`val_smul` 📖	mathematical	—	`val` `Lorentz.ContrMod` `instAddCommGroup` `instAddCommMonoid` `instModuleReal`	—	—

---

← Back to Index