Theorem Submonoid.isUnit_iff_of_ne_zero

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Ideal/Nonunits.lean
feat(Algebra): prerequisites for #31919 (#32118) …
Added Submonoid.isUnit_iff_of_ne_zeroView on Github →