instStarAddMonoid — Mathlib

English

DoubeCentralizer carries a star-additive monoid structure: the star map is additive and involutive on 𝓜(𝕜,A).

Русский

DoubleCentralizer имеет структуру звезда-добавочно-моноида: звезда сохраняет сложение и является инволютивной на 𝓜(𝕜,A).

LaTeX

$$$\\text{instStarAddMonoid}$: звезда сохраняет сложение и инволютивна.$$

Lean4

instance instStarAddMonoid : StarAddMonoid 𝓜(𝕜, A) :=
  {
    DoubleCentralizer.instStar with
    star_involutive := fun x => by ext <;> simp only [star_fst, star_snd, star_star]
    star_add := fun x y => by
      ext <;> simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add] }

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