English
Star-inverse relation: star of inverse equals inverse of star for all invertible elements.
Русский
Относительно звезды: star(inv(r)) = inv(star(r)) для всех инвертируемых элементов.
LaTeX
$$$\star(\,\mathrm{invOf}(r)\,) = \mathrm{invOf}(\star r).$$$
Lean4
theorem star_invOf {R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r] [Invertible (star r)] :
star (⅟r) = ⅟(star r) :=
by
have : star (⅟r) = star (⅟r) * ((star r) * ⅟(star r)) := by simp only [mul_invOf_self, mul_one]
rw [this, ← mul_assoc]
have : (star (⅟r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
rw [this, star_one, one_mul]
