add_mul

Mathlib.SetTheory.Nimber.Field

URI: https://scilib.ai/kg/mathlib#Nimber.add_mul

← MathLib Explorer

English

Nimber multiplication distributes over addition on the right: (a+b)*c = a*c + b*c.

Русский

Умножение Nimber распределяется над сложением справа: (a+b)*c = a*c + b*c.

LaTeX

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

Lean4

protected theorem add_mul (a b c : Nimber) : (a + b) * c = a * c + b * c := by
  rw [Nimber.mul_comm, Nimber.mul_add, Nimber.mul_comm, Nimber.mul_comm b]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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