Theorem Ideal.IsIntegral.comap_ne_bot

Modification history

2026-09-07 13:23

Mathlib/RingTheory/Ideal/GoingUp.lean

chore(RingTheory/Ideal/GoingUp): use `Ideal.under` (#43414) …

Deleted Ideal.IsIntegral.comap_ne_bot View 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.comap_ne_bot View on Github →