right_distrib

Mathlib.NumberTheory.LucasLehmer

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

English

Multiplication distributes over addition on the right: (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 : X q) : (x + y) * z = x * z + y * z := by ext <;> dsimp <;> ring

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

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

Разделы

Аффилиация

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