English
If x is right-regular, then star x is left-regular.
Русский
Если x является правой регулярной, то star x — левой регулярной.
LaTeX
$$$\text{IsRightRegular}(x) \Rightarrow \text{IsLeftRegular}(\star x).$$$
Lean4
protected instance star {R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] : Invertible (star r)
where
invOf := Star.star (⅟r)
invOf_mul_self := by rw [← star_mul, mul_invOf_self, star_one]
mul_invOf_self := by rw [← star_mul, invOf_mul_self, star_one]