isRegular_iff — Mathlib

English

An element a is regular if and only if it is left-regular, under a commuting hypothesis.

Русский

Элемент a регулярен тогда и только тогда, когда он леворегулярен, при условии коммутирования с любым b.

LaTeX

$$IsRegular a ↔ IsLeftRegular a, given ca$$

Lean4

@[to_additive]
theorem isRegular_iff {a : R} (ca : ∀ b, Commute a b) : IsRegular a ↔ IsLeftRegular a :=
  ⟨fun h => h.left, fun h => ⟨h, h.right_of_commute ca⟩⟩

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