Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-27 06:18
413249c6
View on Github →
feat(RingTheory/Artinian):
IsUnit a
iff
a ∈ R⁰
for an artinian ring
R
(
#21084
)
Estimated changes
Modified
Mathlib/RingTheory/Artinian/Ring.lean
added
theorem
IsArtinianRing.isUnit_iff_mem_nonZeroDivisors
added
theorem
IsArtinianRing.isUnit_of_mem_nonZeroDivisors
added
theorem
IsArtinianRing.isUnit_submonoid_eq