OAI/RingTheory/Multiplicity/ReesRootQuotient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ReesRoot.quotientAt line 18
2. def OAI.Lech.ReesRoot.ambientInclusion line 21
3. def OAI.Lech.ReesRoot.quotientProjection line 26
4. lemma OAI.Lech.ReesRoot.ambient_quotient_zero line 31
5. def OAI.Lech.ReesRoot.quotientShortComplex line 42
6. lemma OAI.Lech.ReesRoot.quotientShortComplex_exact line 46
7. def OAI.Lech.ReesRoot.quotientAtRowIso line 60
8. lemma OAI.Lech.ReesRoot.quotientAt_isZero line 66
9. lemma OAI.Lech.ReesRoot.quotientAt_row_bounded line 74