left_distrib

Mathlib.RingTheory.OreLocalization.Ring

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

English

Left distributive law: x · (y + z) = x · y + x · z.

Русский

Левое распределение: x · (y + z) = x · y + x · z.

LaTeX

$$x \cdot (y + z) = x \cdot y + x \cdot z$$

Lean4

protected theorem left_distrib (x y z : R[S⁻¹]) : x * (y + z) = x * y + x * z :=
  OreLocalization.smul_add _ _ _

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

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

Разделы

Аффилиация

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