OAI/Geometry/TamingCompatibility/Hodge/HodgeActualAngular.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinateline 19 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitCoordinate_lineline 25 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateWedge_actualline 35 - def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalAngularline 62 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaNormalWedge_actual_angularline 70