OAI/RingTheory/Multiplicity/CartierQuotientDevissage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.CartierQuotient.quotient line 16
2. lemma OAI.Lech.CartierQuotient.map_power line 20
3. def OAI.Lech.CartierQuotient.step line 25
4. def OAI.Lech.CartierQuotient.reduction line 37
5. lemma OAI.Lech.CartierQuotient.step_reduction line 49
6. def OAI.Lech.CartierQuotient.shortComplex line 61
7. lemma OAI.Lech.CartierQuotient.shortComplex_exact line 64