English
Let R be a semigroup and a ∈ R be left-regular. Then for every b ∈ R, IsLeftRegular(a * b) is equivalent to IsLeftRegular(b).
Русский
Пусть R — полугруппа и a ∈ R — левая регулярность. Тогда для любого b ∈ R выполняется эквивалентность IsLeftRegular(a * b) ⇔ IsLeftRegular(b).
LaTeX
$$$ IsLeftRegular a \rightarrow (IsLeftRegular (a * b) \leftrightarrow IsLeftRegular b) $$$
Lean4
/-- An element is left-regular if and only if multiplying it on the left by a left-regular element
is left-regular. -/
@[to_additive (attr := simp) /-- An element is add-left-regular if and only if adding to it on the
left an add-left-regular element is add-left-regular. -/
]
theorem mul_isLeftRegular_iff (b : R) (ha : IsLeftRegular a) : IsLeftRegular (a * b) ↔ IsLeftRegular b :=
⟨fun ab => IsLeftRegular.of_mul ab, fun ab => IsLeftRegular.mul ha ab⟩
