OAI/Geometry/TamingCompatibility/DifferentialForms/AntiEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.antiInvariantPart_add line 17
2. lemma OAI.TamingCompatibility.antiInvariantPart_smul line 20
3. lemma OAI.TamingCompatibility.ManifoldHodge.starThree_add line 26
4. lemma OAI.TamingCompatibility.ManifoldHodge.starThree_smul line 35
5. lemma OAI.TamingCompatibility.ManifoldHodge.codifferential_anti line 43
6. def OAI.TamingCompatibility.GeometricHilbert.antiPre line 58
7. def OAI.TamingCompatibility.GeometricHilbert.antiDelta line 73
8. def OAI.TamingCompatibility.GeometricHilbert.antiGraph line 97
9. def OAI.TamingCompatibility.GeometricHilbert.antiEnergy line 103
10. instance OAI.TamingCompatibility.GeometricHilbert.antiEnergy_complete line 106