Theorem Ideal.IsIntegral.under_lt_under

Modification history

2026-09-07 13:23

Mathlib/RingTheory/Ideal/GoingUp.lean

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

Added Ideal.IsIntegral.under_lt_under View on Github →