add_smul — Mathlib

English

Let R be a semiring and M an additive commutative monoid with an R-module structure. Then for all r, s in R and x in M, we have (r + s) · x = r · x + s · x.

Русский

Пусть R — полугруппа и M — аддитивный коммутативный моноид, на котором задано действие модуля над R. Тогда для любых r, s ∈ R и x ∈ M выполняется (r + s) · x = r · x + s · x.

LaTeX

$$$\\forall r \\in R\\, \\forall s \\in R\\, \\forall x \\in M,\\ (r + s) \\cdot x = r \\cdot x + s \\cdot x$$$

Lean4

theorem add_smul : (r + s) • x = r • x + s • x :=
  Module.add_smul r s x

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