OAI/RingTheory/Multiplicity/ReesExceptionalSquare.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ReesRoot.graded_square line 22
2. abbrev OAI.Lech.ReesRoot.exceptionalDenominator line 44
3. abbrev OAI.Lech.ReesRoot.ExceptionalRing line 46
4. lemma OAI.Lech.ReesRoot.exceptionalDenominator_mem line 49
5. def OAI.Lech.ReesRoot.chartRename line 55
6. def OAI.Lech.ReesRoot.exceptionalRename line 59
7. def OAI.Lech.ReesRoot.reduction line 65
8. lemma OAI.Lech.ReesRoot.reduction_surjective line 70
9. lemma OAI.Lech.ReesRoot.reduction_mk line 75
10. lemma OAI.Lech.ReesRoot.reduction_eq_zero_iff line 93
11. lemma OAI.Lech.ReesRoot.renamed_reduction_kernel line 99
12. lemma OAI.Lech.ReesRoot.renamed_reduction_zero_iff line 110
13. lemma OAI.Lech.ReesRoot.reduction_kernel line 118