Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `toLorentzGroup`, `toMatrix`, `toRestrictedLorentzGroup`, `toSelfAdjointMap`	4
Theorems `inverse_coe`, `toLorentzGroup_apply_coe`, `toLorentzGroup_det_one`, `toLorentzGroup_eq_pauliBasis'`, `toLorentzGroup_fst_col`, `toLorentzGroup_inl_inl`, `toLorentzGroup_isOrthochronous`, `toMatrix_apply_contrMod`, `toMatrix_mem_lorentzGroup`, `toRestrictedLorentzGroup_apply_coe_coe`, `toSelfAdjointMap_apply_coe`, `toSelfAdjointMap_apply_det`, `toSelfAdjointMap_apply_pauliBasis'_inl`, `toSelfAdjointMap_basis`, `toSelfAdjointMap_pauliBasis`, `transpose_coe`	16
Total	20

Lorentz.SL2C

Definitions

Name	Category	Theorems
`toLorentzGroup` 📖	CompOp	22 math math: `Lorentz.contrContrToMatrix_ρ_symm`, `Lorentz.complexContrBasis_ρ_apply`, `Lorentz.coContrToMatrix_ρ`, `Lorentz.SL2CRep_ρ_basis`, `toLorentzGroup_inl_inl`, `Lorentz.inclCongrRealLorentz_ρ`, `Lorentz.complexCoBasis_ρ_apply`, `Lorentz.coCoToMatrix_ρ`, `toLorentzGroup_apply_coe`, `toLorentzGroup_fst_col`, `toLorentzGroup_det_one`, `toLorentzGroup_isOrthochronous`, `toSelfAdjointMap_pauliBasis`, `realLorentzTensor.toComplex_equivariant`, `Lorentz.coCoToMatrix_ρ_symm`, `Lorentz.contrCoToMatrix_ρ_symm`, `Lorentz.contrCoToMatrix_ρ`, `toLorentzGroup_eq_pauliBasis'`, `toSelfAdjointMap_basis`, `Lorentz.complexContrBasis_ρ_val`, `Lorentz.coContrToMatrix_ρ_symm`, `Lorentz.contrContrToMatrix_ρ`
`toMatrix` 📖	CompOp	4 math math: `toMatrix_apply_contrMod`, `toLorentzGroup_apply_coe`, `toRestrictedLorentzGroup_apply_coe_coe`, `toMatrix_mem_lorentzGroup`
`toRestrictedLorentzGroup` 📖	CompOp	1 math math: `toRestrictedLorentzGroup_apply_coe_coe`
`toSelfAdjointMap` 📖	CompOp	9 math math: `toSelfAdjointMap_apply_det`, `toMatrix_apply_contrMod`, `Fermion.altLeftAltRightToMatrix_ρ_symm_selfAdjoint`, `toSelfAdjointMap_pauliBasis`, `Fermion.leftRightToMatrix_ρ_symm_selfAdjoint`, `toSelfAdjointMap_apply_coe`, `toLorentzGroup_eq_pauliBasis'`, `toSelfAdjointMap_basis`, `toSelfAdjointMap_apply_pauliBasis'_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inverse_coe` 📖	—	—	—	—	—
`toLorentzGroup_apply_coe` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup` `toMatrix`	—	—
`toLorentzGroup_det_one` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`Matrix.schur_triangulation` `toSelfAdjointMap_similar_det` `toSelfAdjointMap_det_one'`
`toLorentzGroup_eq_pauliBasis'` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup` `PauliMatrix.pauliBasis'` `toSelfAdjointMap`	—	—
`toLorentzGroup_fst_col` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`toSelfAdjointMap_apply_pauliBasis'_inl` `toSelfAdjointMap_basis`
`toLorentzGroup_inl_inl` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`toLorentzGroup_fst_col`
`toLorentzGroup_isOrthochronous` 📖	mathematical	—	`LorentzGroup.IsOrthochronous` `LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`LorentzGroup.IsOrthochronous.eq_1` `toLorentzGroup_inl_inl`
`toMatrix_apply_contrMod` 📖	mathematical	—	`Lorentz.ContrMod.mulVec` `toMatrix` `Lorentz.ContrMod` `Lorentz.ContrMod.instAddCommMonoid` `Lorentz.ContrMod.instModuleReal` `Lorentz.ContrMod.toSelfAdjoint` `toSelfAdjointMap`	—	—
`toMatrix_mem_lorentzGroup` 📖	mathematical	—	`LorentzGroup` `toMatrix`	—	`LorentzGroup.mem_iff_norm` `Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint` `toMatrix_apply_contrMod` `toSelfAdjointMap_apply_det`
`toRestrictedLorentzGroup_apply_coe_coe` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.restricted` `toRestrictedLorentzGroup` `toMatrix`	—	—
`toSelfAdjointMap_apply_coe` 📖	mathematical	—	`toSelfAdjointMap`	—	—
`toSelfAdjointMap_apply_det` 📖	mathematical	—	`toSelfAdjointMap`	—	—
`toSelfAdjointMap_apply_pauliBasis'_inl` 📖	mathematical	—	`toSelfAdjointMap` `PauliMatrix.pauliBasis'`	—	`PauliMatrix.pauliSelfAdjoint'_linearly_independent` `PauliMatrix.pauliSelfAdjoint'_span`
`toSelfAdjointMap_basis` 📖	mathematical	—	`toSelfAdjointMap` `PauliMatrix.pauliBasis'` `LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`toLorentzGroup_eq_pauliBasis'`
`toSelfAdjointMap_pauliBasis` 📖	mathematical	—	`toSelfAdjointMap` `PauliMatrix.pauliBasis` `LorentzGroup` `lorentzGroupIsGroup` `toLorentzGroup`	—	`LorentzGroup.dual_mem` `LorentzGroup.inv_eq_dual` `PauliMatrix.pauliBasis_minkowskiMetric_pauliBasis'` `toSelfAdjointMap_basis` `minkowskiMatrix.dual_apply_minkowskiMatrix`
`transpose_coe` 📖	—	—	—	—	—

---

← Back to Index