OAI/RingTheory/Multiplicity/ReesRootQuotientEuler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ReesRoot.enlargedAt_row_bounded line 18
2. lemma OAI.Lech.ReesRoot.total_rectangle_zero line 26
3. lemma OAI.Lech.ReesRoot.quotientAtTotal_bounded line 41
4. lemma OAI.Lech.ReesRoot.enlargedAtTotal_bounded line 50
5. lemma OAI.Lech.ReesRoot.quotientAt_row_finite line 66
6. lemma OAI.Lech.ReesRoot.quotientAt_row_euler line 77
7. lemma OAI.Lech.ReesRoot.quotientAtTotal_finite line 98
8. lemma OAI.Lech.ReesRoot.quotientAtTotal_euler line 109
9. theorem OAI.Lech.ReesRoot.ambient_euler_additive line 128