instStarRing — Mathlib

English

The ring structure on 𝓜(𝕜,A) is compatible with star, i.e., star respects ring product.

Русский

Кольцевая структура на 𝓜(𝕜,A) совместима со звёздой: звезда согласуется с произведением.

LaTeX

$$$\\mathrm{instStarRing}: \\star(x\\cdot y) = \\star(y) \\cdot \\star(x)$$$

Lean4

instance instStarRing : StarRing 𝓜(𝕜, A) :=
  { DoubleCentralizer.instStarAddMonoid with
    star_mul := fun a b => by
      ext <;>
        simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul, Function.comp_apply] }

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