OAI/Algebra/FrobeniusObstruction/ThreeParameters.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundaryOnly.FormalObstruction.ThreeParameters.Poly line 13
2. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.squareIdeal line 15
3. abbrev OAI.BoundaryOnly.FormalObstruction.ThreeParameters.Ring line 18
4. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.s line 20
5. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.w line 22
6. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.s_sq line 24
7. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.topExponent line 29
8. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.topExponent_apply line 31
9. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.topCoeff_ideal line 34
10. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.w_ne_zero line 48
11. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.augmentation line 66
12. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.augmentation_mk line 72
13. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.w_mul_s line 75
14. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.w_mul line 88
15. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.residue_contradiction line 104
16. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.augmentation_s line 115
17. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.augmentation_algebraMap line 118
18. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.nilpotent_sub_augmentation line 124
19. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.isUnit_of_augmentation_ne_zero line 146