add_one_mul

Mathlib.Algebra.Ring.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem add_one_mul [RightDistribClass α] (a b : α) : (a + 1) * b = a * b + b := by rw [add_mul, one_mul]

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

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

Разделы

Аффилиация

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