OAI/Geometry/Relativity/CKS/AreaGram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSArea.Mat2 line 10
2. def OAI.CKSArea.density line 12
3. lemma OAI.CKSArea.real_symmetric line 14
4. lemma OAI.CKSArea.mixed_det_nonneg line 18
5. lemma OAI.CKSArea.det_lower_bound line 35
6. theorem OAI.CKSArea.density_lower_bound line 50