instSMul — Mathlib

English

For s ∈ S and a ∈ 𝓜(𝕜,A), the scalar action commutes with toProd: (s • a).toProd = s • a.toProd.

Русский

Для s ∈ S и a ∈ 𝓜(𝕜,A) скалярное действие коммутирует с toProd: (s • a).toProd = s • a.toProd.

LaTeX

$$$$ (s \\cdot a)^{\\text{toProd}} = s \\cdot a^{\\text{toProd}} $$$$

Lean4

instance instSMul : SMul S 𝓜(𝕜, A) where
  smul s
    a :=
    { toProd := s • a.toProd
      central := fun x y =>
        show (s • a.snd) x * y = x * (s • a.fst) y by
          simp only [ContinuousLinearMap.smul_apply, mul_smul_comm, smul_mul_assoc, central] }

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