OAI/Algebra/FormalGroup/Honda/Classification.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HeightThree.HondaClassification.all_laws_jet2 line 13
2. structure OAI.HeightThree.HondaClassification.Approximation line 19
3. def OAI.HeightThree.HondaClassification.start line 32
4. lemma OAI.HeightThree.HondaClassification.advance_exists line 51
5. def OAI.HeightThree.HondaClassification.advance line 72
6. def OAI.HeightThree.HondaClassification.tower line 76
7. lemma OAI.HeightThree.HondaClassification.tower_step line 80
8. def OAI.HeightThree.HondaJetLimit.limit line 91
9. lemma OAI.HeightThree.HondaJetLimit.later_jet line 93
10. lemma OAI.HeightThree.HondaJetLimit.stable_coeff line 99
11. lemma OAI.HeightThree.HondaJetLimit.limit_jet line 107
12. theorem OAI.HeightThree.HondaClassification.strict_honda_isomorphic line 131