Theorem Polynomial.Monic.quotient_isIntegralElem

Modification history

2024-11-05 13:38
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
feat(RingTheory/IntegralClosure/IsIntegralClosure/Basic): Add lemmas about MvPolynomial and Polynomial (#18244) …
Added Polynomial.Monic.quotient_isIntegralElemView on Github →