instModule — Mathlib

English

For any S acting on N and with appropriate module structures, the Hom-set inherits an S-module structure.

Русский

Для множества гомоморфизмов Hom(M,N) наследуется структура S-модуля при заданных условиях на действия S.

LaTeX

$$Module S (M ⟶ N)$$

Lean4

instance instModule : Module S (M ⟶ N) :=
  Function.Injective.module S { toFun := Hom.hom, map_zero' := hom_zero, map_add' := hom_add } hom_injective
    (fun _ _ => rfl)

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