OAI/Algebra/FormalGroup/Honda/Coordinates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HeightThree.HondaCoordinates.multiplication_zero line 11
2. lemma OAI.HeightThree.HondaCoordinates.multiplication_succ line 13
3. lemma OAI.HeightThree.HondaCoordinates.multiplication_constant line 20
4. lemma OAI.HeightThree.HondaCoordinates.multiplication_map line 30
5. lemma OAI.HeightThree.HondaCoordinates.log_multiplication line 47
6. lemma OAI.HeightThree.HondaCoordinates.multiplication_linear line 59
7. lemma OAI.HeightThree.HondaCoordinates.coeff_pow_below line 75
8. lemma OAI.HeightThree.HondaCoordinates.coeff_pow_leading line 80
9. lemma OAI.HeightThree.HondaCoordinates.coeff_subst_before line 90
10. lemma OAI.HeightThree.HondaCoordinates.coeff_subst_first line 104
11. theorem OAI.HeightThree.HondaCoordinates.multiplication_first_coeff line 127
12. lemma OAI.HeightThree.HondaCoordinates.numerator_one line 157
13. lemma OAI.HeightThree.HondaCoordinates.numerator_two line 161
14. lemma OAI.HeightThree.HondaCoordinates.logarithm_coeff_below line 165
15. lemma OAI.HeightThree.HondaCoordinates.rational_first_cancel line 178
16. theorem OAI.HeightThree.HondaCoordinates.multiplication_first_integral line 188
17. lemma OAI.HeightThree.HondaCoordinates.integralFormalGroup_map line 212
18. theorem OAI.HeightThree.HondaCoordinates.integralFormalGroup_height_one line 219
19. theorem OAI.HeightThree.HondaCoordinates.integralFormalGroup_height_two line 243
20. lemma OAI.HeightThree.HondaCoordinates.numerator_map line 269
21. def OAI.HeightThree.LogarithmicConstruction.StrictLog.map line 292
22. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.formalGroup_map line 299
23. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.ext line 311
24. lemma OAI.HeightThree.HondaCoordinates.logarithm_map line 322
25. lemma OAI.HeightThree.HondaCoordinates.heightThreeLog_map line 341