OAI/RingTheory/Multiplicity/ReesRegular.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.FilteredFraction.chartFraction line 15
2. lemma OAI.Lech.FilteredFraction.chartFraction_apply line 18
3. lemma OAI.Lech.FilteredFraction.chartFraction_injective line 20
4. lemma OAI.Lech.FilteredFraction.chart_smul_injective line 26
5. lemma OAI.Lech.ReesRoot.product_mem line 48
6. lemma OAI.Lech.ReesRoot.denominator_eq line 55
7. theorem OAI.Lech.ReesRoot.coordinate_smul_injective line 61