OAI/RingTheory/Multiplicity/FiniteGradedQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.LinearNormalization.integral_image_of_generators_zero line 12
2. lemma OAI.Lech.LinearNormalization.finite_quotient_of_integral_generators line 28
3. lemma OAI.Lech.LinearNormalization.finite_grading_bounded line 48
4. lemma OAI.Lech.LinearNormalization.high_grades_in_span line 79