OAI/RingTheory/Multiplicity/MinimalReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.MinimalReduction.associatedGraded_nontrivial line 14
2. lemma OAI.Lech.MinimalReduction.pad_generators line 25
3. theorem OAI.Lech.MinimalReduction.exists_reduction line 50
4. lemma OAI.Lech.MinimalReduction.reduction_powers line 88
5. lemma OAI.Lech.MinimalReduction.reduction_power_le line 102
6. lemma OAI.Lech.MinimalReduction.reduction_primary line 107