smul_add — Mathlib

English

PiTensorProduct R s supports a distributive action by a monoid R1, with the usual properties smul_add, one_smul, smul_zero, and mul_smul.

Русский

PiTensorProduct R s поддерживает распределённое действие моноида R1, удовлетворяющее обычным законам smul_add, one_smul, smul_zero, mul_smul.

LaTeX

$$$ (r+r') \cdot x = r \cdot x + r' \cdot x,\quad (r r') \cdot x = r \cdot (r' \cdot x),\quad 1 \cdot x = x,\quad 0 \cdot x = 0. $$$

Lean4

protected theorem smul_add (r : R₁) (x y : ⨂[R] i, s i) : r • (x + y) = r • x + r • y :=
  AddMonoidHom.map_add _ _ _

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