OAI/Algebra/FormalGroup/Honda/Recurrence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HeightThree.HondaConstruction.logarithm_functional_equation line 11
2. def OAI.HeightThree.HondaConstruction.heightThreeLog line 44
3. def OAI.HeightThree.HondaConstruction.integralFormalGroup line 50
4. instance OAI.HeightThree.HondaConstruction.integralFormalGroup_isComm line 59
5. abbrev OAI.HeightThree.HondaConstruction.IntegralBase line 72
6. abbrev OAI.HeightThree.HondaConstruction.RationalBase line 73
7. def OAI.HeightThree.HondaConstruction.coefficientInclusion line 75
8. lemma OAI.HeightThree.HondaConstruction.coefficientInclusion_injective line 78
9. def OAI.HeightThree.HondaConstruction.integralFrobenius line 81
10. def OAI.HeightThree.HondaConstruction.rationalFrobenius line 84
11. lemma OAI.HeightThree.HondaConstruction.frobenius_compatible line 87
12. lemma OAI.HeightThree.HondaConstruction.integralFrobenius_congr line 93
13. def OAI.HeightThree.HondaConstruction.parameters line 100
14. def OAI.HeightThree.HondaConstruction.integralHonda line 102
15. instance OAI.HeightThree.HondaConstruction.integralHonda_isComm line 107
16. def OAI.HeightThree.HondaConstruction.reducedHonda line 111
17. instance OAI.HeightThree.HondaConstruction.mapFormalGroup_isComm line 121
18. instance OAI.HeightThree.HondaConstruction.reducedHonda_isComm line 132