OAI/Geometry/Relativity/CKS/VolumeAlgebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSIntrinsicVolume.stdBasis line 10
2. lemma OAI.CKSIntrinsicVolume.sqrt_gram_det_comp line 12
3. def OAI.CKSIntrinsicVolume.pullbackInner line 26
4. lemma OAI.CKSIntrinsicVolume.chartMatrix_eq_toMatrix line 30