Theorem Ideal.IsIntegral.eq_bot_of_comap_eq_bot

Modification history

2026-09-07 13:23
Mathlib/RingTheory/Ideal/GoingUp.lean
chore(RingTheory/Ideal/GoingUp): use `Ideal.under` (#43414) …
Deleted Ideal.IsIntegral.eq_bot_of_comap_eq_botView on Github →
2026-05-12 10:45
Mathlib/RingTheory/Ideal/GoingUp.lean
chore(RingTheory/Ideal/GoingUp): weaken `IsIntegralClosure` to `Algebra.IsIntegral` (#39070) …
Added Ideal.IsIntegral.eq_bot_of_comap_eq_botView on Github →