OAI/RingTheory/Multiplicity/ExceptionalCoefficientSquare.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.ReesRoot.coefficientDenominator line 14
2. abbrev OAI.Lech.ReesRoot.CoefficientRing line 16
3. lemma OAI.Lech.ReesRoot.coefficientDenominator_mem line 19
4. def OAI.Lech.ReesRoot.coefficientReduction line 23
5. lemma OAI.Lech.ReesRoot.coefficientReduction_one line 27
6. lemma OAI.Lech.ReesRoot.coefficientReduction_mul line 29
7. def OAI.Lech.ReesRoot.coefficientReductionAlg line 33
8. lemma OAI.Lech.ReesRoot.coefficientReduction_surjective line 43
9. lemma OAI.Lech.ReesRoot.coefficientReduction_mk line 47
10. def OAI.Lech.ReesRoot.coefficientTargetRename line 57
11. def OAI.Lech.ReesRoot.coefficientComparison line 63
12. lemma OAI.Lech.ReesRoot.coefficientComparison_mk line 68
13. lemma OAI.Lech.ReesRoot.coefficientComparison_surjective line 80
14. lemma OAI.Lech.ReesRoot.coefficientComparison_kernel line 85
15. lemma OAI.Lech.ReesRoot.coefficientComparison_kernel_zero line 92
16. lemma OAI.Lech.ReesRoot.local_square line 103