smul_add

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#smul_add

English

Another standard zero-scalar action law: 0 • m = 0 for m in A.

Русский

Еще одно стандартное правило: 0 • m = 0 для любых m ∈ A.

LaTeX

$$$\\text{zero\\_smul} \\ (m:\\, A) : (0:\\, M_0) \\cdot m = 0$$$

Lean4

theorem smul_add (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
  DistribSMul.smul_add _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru