mul_add_one

Mathlib.Algebra.Ring.Defs

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

English

In a structure with LeftDistribClass and MulOneClass, a·(b+1) = a·b + a.

Русский

В структуре с левым распределением и единицей умножения, a·(b+1) = a·b + a.

LaTeX

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

Lean4

theorem mul_add_one [LeftDistribClass α] (a b : α) : a * (b + 1) = a * b + a := by rw [mul_add, mul_one]

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

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

Разделы

Аффилиация

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