isUnit_iff_isLeftRegular — Mathlib

English

Let R be an Artinian ring (on the opposite side). An element x ∈ R is a unit if and only if x is left regular (the left multiplication by x is injective).

Русский

Пусть R — артиново кольцо. Элемент x ∈ R является единицей тогда и только тогда, когда он лево-регулярен (левое умножение на x инъективно).

LaTeX

$$$\mathrm{IsUnit}(x) \iff \mathrm{IsLeftRegular}(x)$$$

Lean4

theorem isUnit_iff_isLeftRegular [IsArtinianRing Rᵐᵒᵖ] {x : R} : IsUnit x ↔ IsLeftRegular x := by
  rw [← isRightRegular_op, ← isUnit_op, isUnit_iff_isRightRegular]

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