left_distrib

Mathlib.Algebra.Ring.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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