instSMul — Mathlib

English

There is a scalar action of S on the space of σ₁₂-linear maps M →ₛₗ[σ₁₂] M₂ given by (a • f) defined pointwise by (a • f)(x) = a • f(x).

Русский

Существует скалярное действие множества σ₁₂-линейных отображений M →ₛₗ[σ₁₂] M₂ над S, задаваемое (a • f)(x) = a • f(x).

LaTeX

$$$ (a \cdot f)(x) = a \cdot f(x)$$$

Lean4

instance : SMul S (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun a f ↦
    { toFun := a • (f : M → M₂)
      map_add' := fun x y ↦ by simp only [Pi.smul_apply, f.map_add, smul_add]
      map_smul' := fun c x ↦ by simp [Pi.smul_apply, smul_comm] }⟩

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