OAI/Algebra/FormalGroup/Honda/SpecialFiber.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HeightThree.HondaSpecialFiber.augmentation line 10
2. lemma OAI.HeightThree.HondaSpecialFiber.integerFrobenius line 14
3. def OAI.HeightThree.HondaSpecialFiber.specialParameters line 18
4. def OAI.HeightThree.HondaSpecialFiber.integralSpecial line 20
5. def OAI.HeightThree.HondaSpecialFiber.specialLog line 24
6. lemma OAI.HeightThree.HondaSpecialFiber.integralSpecial_map line 27
7. lemma OAI.HeightThree.HondaSpecialFiber.integralHonda_specialize line 31
8. lemma OAI.HeightThree.HondaSpecialFiber.specialLog_functional line 52
9. lemma OAI.HeightThree.HondaSpecialFiber.specialLog_divided line 71
10. lemma OAI.HeightThree.HondaSpecialFiber.specialLog_p_error line 102
11. lemma OAI.HeightThree.HondaSpecialFiber.integralSpecial_p_split line 129
12. theorem OAI.HeightThree.HondaSpecialFiber.integralSpecial_honda line 165
13. def OAI.HeightThree.HondaSpecialFiber.hondaLaw line 196
14. instance OAI.HeightThree.HondaSpecialFiber.hondaLaw_comm line 199
15. lemma OAI.HeightThree.HondaSpecialFiber.reducedHonda_specialFiber line 205
16. theorem OAI.HeightThree.HondaSpecialFiber.constructed_honda_deformation line 217