right_of_commute — Mathlib

English

If an element a is left-regular and commutes with every b, then it is right-regular.

Русский

Если элемент a является леворегулярным и коммутирует с каждым b, то он является праворегулярным.

LaTeX

$$$\\big(\\forall b,\\mathrm{Commute}(a,b)\\big) \\Rightarrow (\\mathrm{IsLeftRegular}\\ a) \\Rightarrow (\\mathrm{IsRightRegular}\\ a)$$

Lean4

@[to_additive]
theorem right_of_commute {a : R} (ca : ∀ b, Commute a b) (h : IsLeftRegular a) : IsRightRegular a := fun x y xy =>
  h <| (ca x).trans <| xy.trans <| (ca y).symm

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