instStarMulSubtypeMemSubmonoid — Mathlib

English

Star reverses the order of multiplication on unitary elements: star(xy) = star(y) · star(x) for x,y in unitary(R).

Русский

Звезда обращает порядок умножения на унитарных элементах: star(xy) = star(y) · star(x) для x,y ∈ unitary(R).

LaTeX

$$$ \star(xy) = \star(y) \cdot \star(x) $$$

Lean4

instance : StarMul (unitary R) :=
  ⟨by
    intro x y
    ext
    rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]⟩

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