Theorem IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRight

Modification history

2025-10-01 10:39
Mathlib/RingTheory/Artinian/Module.lean
feat(RingTheory): units are exactly non-zerodivisors in noncommutative Artinian rings (#28887)
Added IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRightView on Github →