Theorem IsArtinianRing.isUnit_iff_mem_nonZeroDivisors

Modification history

2025-10-01 10:39
Mathlib/RingTheory/Artinian/Module.lean
feat(RingTheory): units are exactly non-zerodivisors in noncommutative Artinian rings (#28887)
Modified IsArtinianRing.isUnit_iff_mem_nonZeroDivisorsView on Github →
2025-01-27 06:18
Mathlib/RingTheory/Artinian/Ring.lean
feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084)
Added IsArtinianRing.isUnit_iff_mem_nonZeroDivisorsView on Github →