Commit 2024-11-05 13:38 880d71c2
View on Github →feat(RingTheory/IntegralClosure/IsIntegralClosure/Basic): Add lemmas about MvPolynomial and Polynomial (#18244)
This PR proves :
If I is an ideal of the polynomial ring S[X] and contains a monic polynomial f, then S[X]/I is integral over S.
If a ≠ 0, then the degree of X_i in a monomial (MvPolynomial.monomial s) a is equal to s i.
These lemmas will be used to prove the Noether Normalization lemma later.