right_distrib

Mathlib.RingTheory.OreLocalization.Ring

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

English

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

Русский

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

LaTeX

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

Lean4

theorem right_distrib (x y z : R[S⁻¹]) : (x + y) * z = x * z + y * z :=
  OreLocalization.add_smul _ _ _

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

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

Разделы

Аффилиация

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