[Merged by Bors] - feat(RingTheory/Artinian): IsUnit a
iff a ∈ R⁰
for an artinian ring R
#21084
Closed
mistarro wants to merge 2 commits intomasterfrom mistarro/artinian-isunit-nonzerodivisor
+20