Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Co`, `toContr`, `Contr`, `toCo`, `coBasis`, `coBasisFin`, `contrBasis`, `contrBasisFin`, `contrIsoCo`, `instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr`	10
Theorems `ρ_stdBasis`, `coBasisFin_repr_apply`, `coBasisFin_toFin1dℝ`, `coBasis_toFin1dℝ`, `coBasis_ρ_apply`, `continuous_contr`, `contrBasisFin_repr_apply`, `contrBasisFin_toFin1dℝ`, `contrBasis_toFin1dℝ`, `contrBasis_ρ_apply`, `contr_continuous`	11
Total	21

Lorentz

Definitions

Name	Category	Theorems
`Co` 📖	CompOp	34 math math: `coContrToMatrixRe_symm_expand_tmul`, `CoVector.toTensor_symm_pure`, `coContrContract_apply_metric`, `coContrToMatrixRe_ρ_symm`, `preContrCoUnit_apply_one`, `preCoMetricVal_expand_tmul`, `contr_preContrCoUnit`, `contrCoContract_tmul_symm`, `coCoToMatrixRe_symm_expand_tmul`, `coContrToMatrixRe_ρ`, `contrCoContract_basis`, `preCoContrUnitVal_expand_tmul`, `preCoMetric_apply_one`, `coCoToMatrixRe_ρ`, `coBasis_ρ_apply`, `contr_preCoContrUnit`, `coContrContract_hom_tmul`, `coContrContract_basis`, `preCoContrUnit_symm`, `coContrContract_tmul_symm`, `coCoContract_hom_tmul`, `coCoToMatrixRe_ρ_symm`, `coBasisFin_repr_apply`, `coBasisFin_toFin1dℝ`, `contrCoContract_hom_tmul`, `contrCoToMatrixRe_ρ`, `preContrCoUnitVal_expand_tmul`, `contrCoToMatrixRe_symm_expand_tmul`, `preCoContrUnit_apply_one`, `coBasis_toFin1dℝ`, `preContrCoUnit_symm`, `contrCoToMatrixRe_ρ_symm`, `contrCoContract_apply_metric`, `preCoMetricVal_expand_tmul_minkowskiMatrix`
`Contr` 📖	CompOp	62 math math: `contrContrContractField.ge_abs_inner_product`, `coContrToMatrixRe_symm_expand_tmul`, `contrContrContractField.matrix_eq_iff_eq_forall'`, `coContrContract_apply_metric`, `coContrToMatrixRe_ρ_symm`, `contrContrContractField.inl_sq_eq`, `contrContrContractField.matrix_eq_iff_eq_forall`, `Contr.ρ_stdBasis`, `preContrCoUnit_apply_one`, `contrContrContractField.basis_left`, `contrBasis_toFin1dℝ`, `contr_preContrCoUnit`, `contrCoContract_tmul_symm`, `inclCongrRealLorentz_ρ`, `preContrMetricVal_expand_tmul_minkowskiMatrix`, `coContrToMatrixRe_ρ`, `contrContrContractField.matrix_eq_id_iff`, `contrCoContract_basis`, `contrContrContractField.dual_mulVec_right`, `preCoContrUnitVal_expand_tmul`, `continuous_contr`, `contrContrContractField.self_parity_eq_zero_iff`, `contrContrContractField.on_basis`, `preContrMetricVal_expand_tmul`, `contrBasisFin_repr_apply`, `contrBasis_ρ_apply`, `contr_preCoContrUnit`, `coContrContract_hom_tmul`, `coContrContract_basis`, `LorentzGroup.mem_iff_invariant`, `contrContrContractField.le_inl_sq`, `contrContrContractField.matrix_apply_stdBasis`, `preCoContrUnit_symm`, `coContrContract_tmul_symm`, `contrContrContract_hom_tmul`, `contrContrContractField.action_tmul`, `contrContrContractField.as_sum`, `contrContrContractField.nondegenerate`, `contrContrToMatrixRe_symm_expand_tmul`, `contrCoContract_hom_tmul`, `contrBasisFin_toFin1dℝ`, `contrContrToMatrixRe_ρ_symm`, `contrContrContractField.right_parity`, `contrContrContractField.ge_sub_norm`, `contrCoToMatrixRe_ρ`, `contrContrContractField.stdBasis_inl`, `preContrCoUnitVal_expand_tmul`, `contrCoToMatrixRe_symm_expand_tmul`, `contrContrContractField.as_sum_toSpace`, `preCoContrUnit_apply_one`, `contrContrContractField.same_eq_det_toSelfAdjoint`, `contrContrContractField.symm`, `contrContrContractField.matrix_apply_eq_iff_sub`, `contrContrContractField.on_basis_mulVec`, `preContrMetric_apply_one`, `preContrCoUnit_symm`, `contrCoToMatrixRe_ρ_symm`, `contrContrToMatrixRe_ρ`, `LorentzGroup.mem_iff_norm`, `Vector.toTensor_symm_pure`, `contrCoContract_apply_metric`, `contrContrContractField.dual_mulVec_left`
`coBasis` 📖	CompOp	11 math math: `coContrToMatrixRe_symm_expand_tmul`, `preCoMetricVal_expand_tmul`, `coCoToMatrixRe_symm_expand_tmul`, `contrCoContract_basis`, `preCoContrUnitVal_expand_tmul`, `coBasis_ρ_apply`, `coContrContract_basis`, `preContrCoUnitVal_expand_tmul`, `contrCoToMatrixRe_symm_expand_tmul`, `coBasis_toFin1dℝ`, `preCoMetricVal_expand_tmul_minkowskiMatrix`
`coBasisFin` 📖	CompOp	3 math math: `CoVector.toTensor_symm_pure`, `coBasisFin_repr_apply`, `coBasisFin_toFin1dℝ`
`contrBasis` 📖	CompOp	11 math math: `coContrToMatrixRe_symm_expand_tmul`, `contrBasis_toFin1dℝ`, `preContrMetricVal_expand_tmul_minkowskiMatrix`, `contrCoContract_basis`, `preCoContrUnitVal_expand_tmul`, `preContrMetricVal_expand_tmul`, `contrBasis_ρ_apply`, `coContrContract_basis`, `contrContrToMatrixRe_symm_expand_tmul`, `preContrCoUnitVal_expand_tmul`, `contrCoToMatrixRe_symm_expand_tmul`
`contrBasisFin` 📖	CompOp	3 math math: `contrBasisFin_repr_apply`, `contrBasisFin_toFin1dℝ`, `Vector.toTensor_symm_pure`
`contrIsoCo` 📖	CompOp	—
`instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr` 📖	CompOp	2 math math: `contr_continuous`, `continuous_contr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coBasisFin_repr_apply` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `coBasisFin` `CoMod.val`	—	—
`coBasisFin_toFin1dℝ` 📖	mathematical	—	`CoMod.toFin1dℝ` `LorentzGroup` `lorentzGroupIsGroup` `Co` `coBasisFin`	—	`coBasis_toFin1dℝ`
`coBasis_toFin1dℝ` 📖	mathematical	—	`CoMod.toFin1dℝ` `LorentzGroup` `lorentzGroupIsGroup` `Co` `coBasis`	—	—
`coBasis_ρ_apply` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `coBasis`	—	—
`continuous_contr` 📖	mathematical	`ContrMod.toFin1dℝ`	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr`	—	—
`contrBasisFin_repr_apply` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrBasisFin` `ContrMod.val`	—	—
`contrBasisFin_toFin1dℝ` 📖	mathematical	—	`ContrMod.toFin1dℝ` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrBasisFin`	—	`contrBasis_toFin1dℝ`
`contrBasis_toFin1dℝ` 📖	mathematical	—	`ContrMod.toFin1dℝ` `LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrBasis`	—	—
`contrBasis_ρ_apply` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrBasis`	—	—
`contr_continuous` 📖	mathematical	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `ContrMod` `ContrMod.instAddCommMonoid` `ContrMod.instModuleReal` `ContrMod.toFin1dℝEquiv`	`instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr`	—	`ContrMod.toFin1dℝEquiv_isInducing`

Lorentz.Co

Definitions

Name	Category	Theorems
`toContr` 📖	CompOp	—

Lorentz.Contr

Definitions

Name	Category	Theorems
`toCo` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ρ_stdBasis` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Lorentz.Contr` `Lorentz.ContrMod` `Lorentz.ContrMod.instAddCommMonoid` `Lorentz.ContrMod.instModuleReal` `Lorentz.ContrMod.stdBasis` `Lorentz.ContrMod.instAddCommGroup`	—	`Lorentz.ContrMod.ext`

---

← Back to Index