Theorem Polynomial.Monic.quotient_isIntegral

Modification history

2024-12-21 08:53
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
chore: tidy various files (#20130)
Modified Polynomial.Monic.quotient_isIntegralView on Github →
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_isIntegralView on Github →