instModule — Mathlib

English

The zero-Hom space from A to B is a module over R given appropriate semiring and module structures.

Русский

Пространство нулевых гомоморфизмов From A to B образует модуль над R при заданных структурах полукольца и модуля.

LaTeX

$$$$ \\text{ZeroHom}(A,B) \text{ is an } R\text{-module}. $$$$

Lean4

instance instModule [Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] : Module R (ZeroHom A B)
    where
  __ : MulActionWithZero _ _ := ZeroHom.instMulActionWithZero
  add_smul _ _ _ := ext fun _ => add_smul _ _ _
  smul_add _ _ _ := ext fun _ => smul_add _ _ _

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