OAI/Algebra/FormalGroup/Honda/IntegralLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HeightThree.HondaConstruction.law_integral line 12
2. lemma OAI.HeightThree.HondaConstruction.map_injective line 26
3. def OAI.HeightThree.HondaConstruction.descendFormalGroup line 33
4. theorem OAI.HeightThree.HondaConstruction.map_descendFormalGroup line 54
5. instance OAI.HeightThree.HondaConstruction.descendFormalGroup_isComm line 60
6. def OAI.HeightThree.HondaConstruction.numerator line 78
7. def OAI.HeightThree.HondaConstruction.logarithm line 84
8. lemma OAI.HeightThree.HondaConstruction.logarithm_constant line 88
9. lemma OAI.HeightThree.HondaConstruction.logarithm_linear line 92
10. lemma OAI.HeightThree.HondaConstruction.twisted_series_coeff line 97
11. lemma OAI.HeightThree.HondaConstruction.twisted_series_coeff_outside line 110
12. lemma OAI.HeightThree.HondaConstruction.iterate_smul line 128
13. lemma OAI.HeightThree.HondaConstruction.iterate_comp line 137
14. lemma OAI.HeightThree.HondaConstruction.scalar_denominator line 148
15. lemma OAI.HeightThree.HondaConstruction.logarithm_recurrence line 163