right_distrib

Mathlib.Algebra.Ring.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem right_distrib [Mul R] [Add R] [RightDistribClass R] (a b c : R) : (a + b) * c = a * c + b * c :=
  RightDistribClass.right_distrib a b c

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

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

Разделы

Аффилиация

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