instStarModule — Mathlib

English

There is a StarModule structure on 𝓜(𝕜,A) with respect to 𝕜-action and the star operation.

Русский

На 𝓜(𝕜,A) задаётся структура StarModule по отношению к 𝕜-действию и звездной операции.

LaTeX

$$$\\text{instStarModule}: StarModule 𝕜 𝓜(𝕜,A)$$$

Lean4

instance instStarModule : StarModule 𝕜 𝓜(𝕜, A) :=
  { DoubleCentralizer.instStarAddMonoid (𝕜 := 𝕜) (A := A) with star_smul := fun k a => by ext <;> exact star_smul _ _ }

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