mul_sub_one

Mathlib.Algebra.Ring.Defs

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

English

In any ring, for all a, b, one has a(b−1) = ab − a.

Русский

В любом кольце для любых a, b выполняется a·(b−1) = a·b − a.

LaTeX

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

Lean4

theorem mul_sub_one (a b : α) : a * (b - 1) = a * b - a := by rw [mul_sub, mul_one]

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

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

Разделы

Аффилиация

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