English
Let R be a semigroup. If b * a is right-regular, then b is right-regular.
Русский
Пусть R — полугруппа. Если b * a является праворегулярным, то b является праворегулярным.
LaTeX
$$$ IsRightRegular (b * a) \rightarrow IsRightRegular b $$$
Lean4
/-- If an element `b` becomes right-regular after multiplying it on the right by a right-regular
element, then `b` is right-regular. -/
@[to_additive /-- If an element `b` becomes add-right-regular after adding to it on the right
an add-right-regular element, then `b` is add-right-regular. -/
]
theorem of_mul (ab : IsRightRegular (b * a)) : IsRightRegular b :=
by
refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))
rw [← mul_assoc, ← mul_assoc]
exact congr_arg (· * a) xy
