OAI/Geometry/Relativity/CKS/CollarRawDEC.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.coordinateDEC line 12
2. lemma OAI.CKSAngularGeometry.commonAngularMomentum_norm_sq line 17
3. lemma OAI.CKSAngularGeometry.coordinateDEC_iff line 30
4. theorem OAI.CKSAngularGeometry.bounded_raw_DEC line 37