OAI/Geometry/TamingCompatibility/DifferentialForms/InnerJLeft.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.UnitaryBasis.inner_J_left line 26
2. lemma OAI.TamingCompatibility.UnitaryBasis.inner_self_J line 32
3. lemma OAI.TamingCompatibility.UnitaryBasis.unit_pair line 38
4. theorem OAI.TamingCompatibility.UnitaryBasis.exists_unitary_basis line 47
5. abbrev OAI.TamingCompatibility.GeometricSymbol.TwoForm line 104
6. def OAI.TamingCompatibility.GeometricSymbol.coords line 107
7. lemma OAI.TamingCompatibility.GeometricSymbol.eval_swap line 111
8. lemma OAI.TamingCompatibility.GeometricSymbol.eval_self line 117
9. lemma OAI.TamingCompatibility.GeometricSymbol.coords_injective line 120
10. def OAI.TamingCompatibility.GeometricSymbol.symbol line 145
11. lemma OAI.TamingCompatibility.GeometricSymbol.symbol_apply line 148
12. lemma OAI.TamingCompatibility.GeometricSymbol.eval_left line 163
13. lemma OAI.TamingCompatibility.GeometricSymbol.coords_symbol line 170
14. def OAI.TamingCompatibility.GeometricSymbol.antiInvariant line 186
15. lemma OAI.TamingCompatibility.GeometricSymbol.eval_neg_left line 189
16. lemma OAI.TamingCompatibility.GeometricSymbol.eval_neg_right line 193
17. lemma OAI.TamingCompatibility.GeometricSymbol.coords_antiInvariant line 196
18. lemma OAI.TamingCompatibility.GeometricSymbol.coords_smul line 210
19. theorem OAI.TamingCompatibility.GeometricSymbol.closed_lift_principal_symbol line 214