Theorem Ring.DimensionLEOne.of_isIntegral

Modification history

2026-05-12 10:45
Mathlib/RingTheory/DedekindDomain/Basic.lean
chore(RingTheory/Ideal/GoingUp): weaken `IsIntegralClosure` to `Algebra.IsIntegral` (#39070) …
Added Ring.DimensionLEOne.of_isIntegralView on Github →