OAI/Geometry/TamingCompatibility/Hodge/HodgeIntrinsicUnitLine.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_intrinsic_unit_line line 21
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.rawVector_pairing line 60
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.rawVector_constant_test line 69
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.rawVector_star line 77
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_coordinateEncode line 90
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_unitDual_raw_line line 100
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_unitDual_coordinate_line line 116
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitDual_starDirection line 158
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateWedge_lines line 169