OAI/Geometry/TamingCompatibility/DifferentialForms/AntiInvariantFrame.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.AntiInvariantFrame.covectorWedge line 15
2. lemma OAI.TamingCompatibility.AntiInvariantFrame.covectorWedge_apply line 18
3. def OAI.TamingCompatibility.AntiInvariantFrame.realPart line 23
4. def OAI.TamingCompatibility.AntiInvariantFrame.imagPart line 26
5. lemma OAI.TamingCompatibility.AntiInvariantFrame.realPart_apply line 31
6. lemma OAI.TamingCompatibility.AntiInvariantFrame.imagPart_apply line 37
7. lemma OAI.TamingCompatibility.AntiInvariantFrame.frame_ext line 43
8. lemma OAI.TamingCompatibility.AntiInvariantFrame.eval_neg_left line 63
9. lemma OAI.TamingCompatibility.AntiInvariantFrame.eval_neg_right line 66
10. lemma OAI.TamingCompatibility.AntiInvariantFrame.eval_self line 69
11. lemma OAI.TamingCompatibility.AntiInvariantFrame.realPart_antiInvariant line 79
12. lemma OAI.TamingCompatibility.AntiInvariantFrame.imagPart_antiInvariant line 86
13. lemma OAI.TamingCompatibility.AntiInvariantFrame.expansion line 94
14. lemma OAI.TamingCompatibility.AntiInvariantFrame.realPart_smooth line 121
15. lemma OAI.TamingCompatibility.AntiInvariantFrame.imagPart_smooth line 138