OAI/RingTheory/Multiplicity/LinearNormalization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.LinearNormalization.homogeneous_top_coeff line 13
2. lemma OAI.Lech.LinearNormalization.homogeneous_relation line 35
3. lemma OAI.Lech.LinearNormalization.exists_homogeneous_direction line 65
4. def OAI.Lech.LinearNormalization.linearChange line 72
5. lemma OAI.Lech.LinearNormalization.linearChange_homogeneous line 76
6. lemma OAI.Lech.LinearNormalization.linearChange_eval line 89
7. lemma OAI.Lech.LinearNormalization.linearChange_leadingCoeff line 97
8. lemma OAI.Lech.LinearNormalization.finSucc_aeval line 112
9. lemma OAI.Lech.LinearNormalization.linearChange_substitution line 121
10. lemma OAI.Lech.LinearNormalization.integral_over_reduced_generators line 134