OAI/Algebra/FormalGroup/Honda/Rigidity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HeightThree.DeformationRigidity.multiplication_zero line 10
2. lemma OAI.HeightThree.DeformationRigidity.multiplication_succ line 13
3. lemma OAI.HeightThree.DeformationRigidity.multiplication_constant line 20
4. lemma OAI.HeightThree.DeformationRigidity.multiplication_map line 30
5. def OAI.HeightThree.DeformationRigidity.SquareZeroKernel line 53
6. lemma OAI.HeightThree.DeformationRigidity.subst_eq_of_squareZero line 56
7. lemma OAI.HeightThree.DeformationRigidity.mul_eq_zero_of_map_zero line 75
8. lemma OAI.HeightThree.DeformationRigidity.highPower_unchanged line 85
9. lemma OAI.HeightThree.DeformationRigidity.subst_after_mv line 98
10. lemma OAI.HeightThree.DeformationRigidity.coordinate_add line 104
11. lemma OAI.HeightThree.DeformationRigidity.law_pair_subst line 131
12. lemma OAI.HeightThree.DeformationRigidity.coordinate_multiplication line 143
13. lemma OAI.HeightThree.DeformationRigidity.subst_near_X_highPower line 157
14. lemma OAI.HeightThree.DeformationRigidity.infinitesimal_pseries line 175
15. theorem OAI.HeightThree.DeformationRigidity.infinitesimal_automorphism_rigid line 201