Theorem Ideal.IsIntegral.under_ne_bot

Modification history

2026-09-07 13:23

Mathlib/RingTheory/Ideal/GoingUp.lean

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

Added Ideal.IsIntegral.under_ne_bot View on Github →