OAI/Algebra/FormalGroup/Honda/HeightTwo.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HeightThree.HondaCoordinates.killFirstFun line 11
2. lemma OAI.HeightThree.HondaCoordinates.coeff_killFirstFun line 14
3. def OAI.HeightThree.HondaCoordinates.killFirst line 17
4. lemma OAI.HeightThree.HondaCoordinates.coeff_killFirst line 64
5. lemma OAI.HeightThree.HondaCoordinates.killFirst_X_zero line 67
6. lemma OAI.HeightThree.HondaCoordinates.killFirst_X_one line 75
7. lemma OAI.HeightThree.HondaCoordinates.killFirst_eq_zero_iff line 83
8. lemma OAI.HeightThree.HondaCoordinates.map_killFirst line 94
9. lemma OAI.HeightThree.HondaCoordinates.expand_killFirst line 100
10. lemma OAI.HeightThree.HondaCoordinates.formalGroup_map_map line 121
11. lemma OAI.HeightThree.HondaCoordinates.formalGroup_map_injective line 126
12. lemma OAI.HeightThree.HondaCoordinates.integralFormalGroup_natural line 133
13. lemma OAI.HeightThree.HondaCoordinates.killFirst_inclusion line 150
14. lemma OAI.HeightThree.HondaCoordinates.killFirst_commute_integralFrobenius line 156
15. lemma OAI.HeightThree.HondaCoordinates.integralHonda_killFirst line 162
16. lemma OAI.HeightThree.HondaCoordinates.integralHonda_height_two line 171
17. theorem OAI.HeightThree.HondaCoordinates.reducedHonda_height_one line 186
18. theorem OAI.HeightThree.HondaCoordinates.reducedHonda_heightCoordinates line 207