OAI/Geometry/TamingCompatibility/Hodge/HodgeDifferentialLocality.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ComplexMatrix.fullShiftedSquare_cutoff_locality line 18
2. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_cutoff_locality line 32
3. def OAI.TamingCompatibility.ComplexMatrix.LocallyEqual line 45
4. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_local_congr line 49
5. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.refl line 61
6. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.symm line 64
7. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.trans line 67
8. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.sub line 71
9. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.fiberMap line 76
10. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_power_local_congr line 82
11. lemma OAI.TamingCompatibility.ComplexMatrix.triple_product_cancel line 95
12. def OAI.TamingCompatibility.ComplexMatrix.antiMatrix line 121
13. lemma OAI.TamingCompatibility.ComplexMatrix.antiMatrix_embed line 125
14. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_antiInvariant line 135
15. lemma OAI.TamingCompatibility.HodgeChart.rawVector_antiInvariantPart line 159
16. lemma OAI.TamingCompatibility.HodgeChart.complex_rawVector_antiInvariantPart line 167