Documentation Verification Report

Proper

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

Statistics

Metric	Count
Definitions `IsProper`, `coeForℤ₂`, `detContinuous`, `detRep`, `instDecidablePredElemMatrixSumFinOfNatNatRealIsProper`, `instTopologicalSpaceMultiplicativeZModOfNatNat`	6
Theorems `coeForℤ₂_apply`, `detContinuous_eq_iff_det_eq`, `detContinuous_eq_one`, `detContinuous_eq_zero`, `detRep_apply`, `detRep_continuous`, `detRep_on_connected_component`, `det_eq_one_or_neg_one`, `det_of_joined`, `det_on_connected_component`, `instDiscreteTopologyMultiplicativeZModOfNatNat`, `instIsTopologicalGroupMultiplicativeZModOfNatNat`, `isProper_id`, `isProper_iff`, `isProper_mul`, `isProper_on_connected_component`	16
Total	22

LorentzGroup

Definitions

Name	Category	Theorems
`IsProper` 📖	MathDef	6 math math: `mem_rotations_iff`, `generalizedBoost_isProper`, `lorentzAlgebra.exp_isProper`, `isProper_iff`, `isProper_on_connected_component`, `isProper_id`
`coeForℤ₂` 📖	CompOp	1 math math: `coeForℤ₂_apply`
`detContinuous` 📖	CompOp	4 math math: `detRep_apply`, `detContinuous_eq_one`, `detContinuous_eq_iff_det_eq`, `detContinuous_eq_zero`
`detRep` 📖	CompOp	4 math math: `detRep_apply`, `detRep_on_connected_component`, `isProper_iff`, `detRep_continuous`
`instDecidablePredElemMatrixSumFinOfNatNatRealIsProper` 📖	CompOp	—
`instTopologicalSpaceMultiplicativeZModOfNatNat` 📖	CompOp	10 math math: `orthchroMap_not_IsOrthochronous`, `instDiscreteTopologyMultiplicativeZModOfNatNat`, `coeForℤ₂_apply`, `instIsTopologicalGroupMultiplicativeZModOfNatNat`, `detRep_apply`, `orthchroMap_IsOrthochronous`, `detContinuous_eq_one`, `detRep_continuous`, `detContinuous_eq_iff_det_eq`, `detContinuous_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeForℤ₂_apply` 📖	mathematical	—	`instTopologicalSpaceMultiplicativeZModOfNatNat` `coeForℤ₂`	—	—
`detContinuous_eq_iff_det_eq` 📖	mathematical	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `detContinuous`	—	`det_eq_one_or_neg_one` `detContinuous_eq_one` `detContinuous_eq_zero`
`detContinuous_eq_one` 📖	mathematical	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `detContinuous`	—	—
`detContinuous_eq_zero` 📖	mathematical	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `detContinuous`	—	`det_eq_one_or_neg_one`
`detRep_apply` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `detRep` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `detContinuous`	—	—
`detRep_continuous` 📖	mathematical	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `lorentzGroupIsGroup` `detRep`	—	—
`detRep_on_connected_component` 📖	mathematical	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup`	`lorentzGroupIsGroup` `detRep`	—	`det_on_connected_component`
`det_eq_one_or_neg_one` 📖	mathematical	—	`LorentzGroup`	—	`minkowskiMatrix.det_dual` `mem_iff_self_mul_dual`
`det_of_joined` 📖	mathematical	—	`LorentzGroup`	—	`det_on_connected_component`
`det_on_connected_component` 📖	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup`	—	—	`instDiscreteTopologyMultiplicativeZModOfNatNat`
`instDiscreteTopologyMultiplicativeZModOfNatNat` 📖	mathematical	—	`instTopologicalSpaceMultiplicativeZModOfNatNat`	—	—
`instIsTopologicalGroupMultiplicativeZModOfNatNat` 📖	mathematical	—	`instTopologicalSpaceMultiplicativeZModOfNatNat`	—	`instDiscreteTopologyMultiplicativeZModOfNatNat`
`isProper_id` 📖	mathematical	—	`IsProper` `LorentzGroup` `lorentzGroupIsGroup`	—	—
`isProper_iff` 📖	mathematical	—	`IsProper` `LorentzGroup` `lorentzGroupIsGroup` `detRep`	—	`detRep_apply` `detContinuous_eq_iff_det_eq`
`isProper_mul` 📖	mathematical	`IsProper`	`LorentzGroup` `lorentzGroupIsGroup`	—	`IsProper.eq_1` `lorentzGroupIsGroup_mul_coe`
`isProper_on_connected_component` 📖	mathematical	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup`	`IsProper`	—	`det_on_connected_component`

---

← Back to Index