isUnit_of_mem_nonZeroDivisors_of_mulOpposite

English

If a ∈ R⁰, then a is a unit when R is Artinian, even in the opposite ring context.

Русский

Если a ∈ R⁰, то при артиновом кольце a является единицей, даже в контексте противоположного кольца.

LaTeX

$$$a \in \mathrm{NZD}(R) \Rightarrow \mathrm{IsUnit}(a) \quad (R\text{ Artinian})$$$

Lean4

theorem isUnit_of_mem_nonZeroDivisors_of_mulOpposite [IsArtinianRing Rᵐᵒᵖ] {a : R} (ha : a ∈ R⁰) : IsUnit a := by
  rwa [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]

Похожие утверждения