OAI/Geometry/Relativity/CKS/LogPhysicalMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMixedGeometry.traceProduct_sub line 12
2. lemma OAI.CKSMixedGeometry.traceProduct_inverse_smul line 15
3. def OAI.CKSMixedGeometry.logExpansion line 23
4. lemma OAI.CKSMixedGeometry.log_lie_coefficient line 27
5. lemma OAI.CKSMixedGeometry.log_expansion_coefficient line 46
6. def OAI.CKSMixedGeometry.logPhysicalMass line 90
7. lemma OAI.CKSMixedGeometry.log_physical_mass_eq line 94