OAI/Geometry/TamingCompatibility/DifferentialForms/TestLinear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldForms.chartLift_add line 16
2. lemma OAI.TamingCompatibility.GeometricChart.coordinateTest_add line 31
3. lemma OAI.TamingCompatibility.GeometricChart.manifoldTest_add line 36
4. def OAI.TamingCompatibility.ComplexMatrix.realComponent line 46
5. lemma OAI.TamingCompatibility.ComplexMatrix.realComponent_apply line 48
6. lemma OAI.TamingCompatibility.ComplexMatrix.realComponent_support line 50
7. lemma OAI.TamingCompatibility.ComplexMatrix.pair_decompose line 53
8. lemma OAI.TamingCompatibility.GeometricHilbert.pair_all_tests_eq line 72