OAI/RingTheory/Multiplicity/ProjectiveReduction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.CoefficientReduction.grade line 13
2. def OAI.Lech.CoefficientReduction.graded line 15
3. lemma OAI.Lech.CoefficientReduction.graded_smul line 21
4. lemma OAI.Lech.CoefficientReduction.graded_surjective line 25
5. lemma OAI.Lech.CoefficientReduction.homogeneous_mem_smul line 30
6. def OAI.Lech.CoefficientReduction.chartMap line 58
7. lemma OAI.Lech.CoefficientReduction.chartMap_surjective line 63
8. lemma OAI.Lech.CoefficientReduction.target_scalar_zero line 66
9. lemma OAI.Lech.CoefficientReduction.chartMap_kernel line 76
10. def OAI.Lech.CoefficientReduction.chartQuotientEquiv line 93