non-units in artinian ring

Stream: Is there code for X?

[Edison Xie]

Do we have that every non-unit in an artinian ring is a zero-divisor?

[Junyan Xu]

For commutative artinian rings, use MaximalSpectrum.toPiLocalizationEquiv and isArtinianRing_iff_isNilpotent_maximalIdeal.

[Junyan Xu]

Oh it's probably quicker to use IsArtinian.surjective_of_injective_endomorphism.

[Edison Xie]

Junyan Xu said:

For commutative artinian rings, use MaximalSpectrum.toPiLocalizationEquiv and isArtinianRing_iff_isNilpotent_maximalIdeal.

Ah thanks but sadly my ring is not commutative :-(

[Junyan Xu]

The latter argument applies more generally: if r is not a left zero-divisor, then left multiplication by r is injective, and since it's an endomorphism of R as a right R-module, we conclude that it's bijective if R is right Artinian, so r has a right inverse is a unit. Similarly if r is not a right zero-divisor and R is left Artinian, then r has a left inverse is a unit. Combining both, if r is either a left or right non-zero-divisor and R is (two-sided) Artinian (e.g. if it's semisimple), then r is a unit. Alternatively, if r ∈ nonZeroDivisors R and R is left or right Artinian, then r is a unit.
(This can be generalized to Artinian semirings if nonZeroDivisors is replaced by IsRegular.)

[Junyan Xu]

Wait, we actually have IsUnit.isUnit_iff_mulLeft_bijective. I've corrected the above post.
Forgot to say, Grok Expert mode told me this proof after thinking 3m27s (it's answers are generally a lot shorter than Gemini 2.5 Pro).
I can submit a PR later today.

[Junyan Xu]

Not sure if I included a form that you want but I opened #28887

[Junyan Xu]

I found IsArtinianRing.isUnit_of_mem_nonZeroDivisors and nearby lemmas which should probably be generalized ...