OAI/Combinatorics/SumProduct/Alignment/RationalEchelon01.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AllLevelFactorization.Factorization.physical_pivot_empirical_success_mass line 49
2. def OAI.CubeFaces.vertexMap line 103
3. lemma OAI.CubeFaces.vertexMap_apply line 109
4. lemma OAI.CubeFaces.vertexMap_face line 112
5. lemma OAI.CubeFaces.map_cube line 118
6. lemma OAI.CubeFaces.exists_cube_lift line 124
7. structure OAI.RationalEchelon.Chart line 148
8. def OAI.RationalEchelon.dropLast line 158
9. def OAI.RationalEchelon.snocZero line 163
10. lemma OAI.RationalEchelon.expansion line 168
11. lemma OAI.RationalEchelon.lift line 174
12. theorem OAI.RationalEchelon.chart_exists line 197