Theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_under

Modification history

2026-09-07 13:23
Mathlib/RingTheory/Ideal/GoingUp.lean
chore(RingTheory/Ideal/GoingUp): use `Ideal.under` (#43414) …
Added Ideal.isMaximal_of_isIntegral_of_isMaximal_underView on Github →