star — Mathlib

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]

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