OAI/Geometry/TamingCompatibility/DifferentialForms/Star.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HodgeThree.star line 30
2. lemma OAI.TamingCompatibility.HodgeThree.star_apply line 34
3. lemma OAI.TamingCompatibility.HodgeThree.volume_on_frame line 46
4. lemma OAI.TamingCompatibility.HodgeThree.star_on_frame line 63
5. lemma OAI.TamingCompatibility.HodgeThree.star_injective_frame line 70
6. lemma OAI.TamingCompatibility.HodgeThree.star_injective line 82
7. lemma OAI.TamingCompatibility.HodgeThree.star_zero line 88
8. lemma OAI.TamingCompatibility.HodgeThree.star_eq_zero line 95
9. structure OAI.TamingCompatibility.MetricModel.Metric line 108
10. def OAI.TamingCompatibility.MetricModel.Model line 115
11. instance OAI.TamingCompatibility.MetricModel.(instance at line 117) line 117
12. instance OAI.TamingCompatibility.MetricModel.(instance at line 118) line 118
13. instance OAI.TamingCompatibility.MetricModel.(instance at line 119) line 119
14. instance OAI.TamingCompatibility.MetricModel.core line 122
15. instance OAI.TamingCompatibility.MetricModel.(instance at line 141) line 141
16. instance OAI.TamingCompatibility.MetricModel.(instance at line 144) line 144
17. lemma OAI.TamingCompatibility.MetricModel.model_inner line 147
18. def OAI.TamingCompatibility.MetricModel.ofOriginal line 149
19. def OAI.TamingCompatibility.MetricModel.toOriginal line 151
20. def OAI.TamingCompatibility.MetricModel.linearEquiv line 153
21. def OAI.TamingCompatibility.MetricModel.equiv line 155
22. lemma OAI.TamingCompatibility.MetricModel.equiv_apply line 158
23. lemma OAI.TamingCompatibility.MetricModel.equiv_symm_apply line 159
24. lemma OAI.TamingCompatibility.MetricModel.finrank_model line 161
25. def OAI.TamingCompatibility.MetricModel.isometry line 164
26. lemma OAI.TamingCompatibility.MetricModel.isometry_apply line 178