Theorem Ideal.notMem_of_isUnit

Modification history

2026-02-10 18:25
Mathlib/RingTheory/Ideal/Prime.lean
feat(RingTheory): etale local structure of quasi-finite algebras (#35036)
Added Ideal.notMem_of_isUnitView on Github →