distrib_three_right — Mathlib

English

For a,b,c,d in a structure with Mul, Add and RightDistribClass, (a+b+c)·d = a·d + b·d + c·d.

Русский

Для a,b,c,d в структуре с умножением и сложением и RightDistribClass выполняется (a+b+c)·d = a·d + b·d + c·d.

LaTeX

$$$ (a + b + c) \cdot d = a \cdot d + b \cdot d + c \cdot d $$$

Lean4

theorem distrib_three_right [Mul R] [Add R] [RightDistribClass R] (a b c d : R) :
    (a + b + c) * d = a * d + b * d + c * d := by simp [right_distrib]

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