instSMulHom — Mathlib

English

The morphism set Hom(S1,S2) carries an R-module structure defined by scaling the morphism components τ1, τ2, τ3 by a.

Русский

Множество гомоморфизмов Hom(S1,S2) обладает структурой модуля над R, задаваемой умножением компонент τ1, τ2, τ3 на скаляр a.

LaTeX

$$$\text{SMul}_R(\mathrm{Hom}(S_1,S_2))$$$

Lean4

instance : SMul R (S₁ ⟶ S₂) where
  smul a
    φ :=
    { τ₁ := a • φ.τ₁
      τ₂ := a • φ.τ₂
      τ₃ := a • φ.τ₃ }

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