OAI/Algebra/FormalGroup/Honda/NilpotentTower.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HeightThree.NilpotentTower.quotient line 10
2. instance OAI.HeightThree.NilpotentTower.(instance at line 12) line 12
3. instance OAI.HeightThree.NilpotentTower.(instance at line 13) line 13
4. def OAI.HeightThree.NilpotentTower.projection line 15
5. def OAI.HeightThree.NilpotentTower.augmentation line 18
6. lemma OAI.HeightThree.NilpotentTower.augmentation_projection line 21
7. lemma OAI.HeightThree.NilpotentTower.projection_surjective line 24
8. lemma OAI.HeightThree.NilpotentTower.projection_eq_zero line 27
9. lemma OAI.HeightThree.NilpotentTower.augmentation_ker line 30
10. lemma OAI.HeightThree.NilpotentTower.augmentation_nilpotent line 41
11. lemma OAI.HeightThree.NilpotentTower.projection_ker_le line 47
12. lemma OAI.HeightThree.NilpotentTower.projection_annihilate line 51
13. lemma OAI.HeightThree.NilpotentTower.nilpotent_of_mem_ker line 58
14. lemma OAI.HeightThree.NilpotentTower.augmentation_surjective line 65
15. lemma OAI.HeightThree.NilpotentTower.finite_local_nilpotent line 69