OAI/Geometry/TamingCompatibility/Hodge/HodgeUnitDual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitFrameDirection line 24
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitDual line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_direction line 37
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.unitDual_pairing line 62
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairingEvaluation_unitDual line 73
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairingEvaluationVector_unitDual line 89
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairingHeatVector_unitDual line 94
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairingGammaTail_unitDual line 100