OAI/Geometry/TamingCompatibility/Hodge/HodgeDirectionCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_swap line 13
2. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_sum_left line 21
3. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_smul_left line 30
4. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_sum_right line 34
5. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_smul_right line 42
6. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_self line 47
7. lemma OAI.TamingCompatibility.UnitaryFrame.alternating_frame_eval line 50
8. def OAI.TamingCompatibility.HodgeFrame.directionCoordinates line 69
9. lemma OAI.TamingCompatibility.HodgeFrame.directionCoordinates_apply line 74
10. lemma OAI.TamingCompatibility.HodgeFrame.sum_directionCoordinates line 80
11. lemma OAI.TamingCompatibility.HodgeFrame.norm_directionCoordinates line 87
12. lemma OAI.TamingCompatibility.HodgeFrame.complex_frame_sum line 97
13. lemma OAI.TamingCompatibility.HodgeFrame.directionCoordinates_eval line 104
14. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_eq_six line 126
15. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_direction_eval line 133