mul_left_cancel

Mathlib.Algebra.Group.Defs

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

English

If a*b = a*c then b=c.

Русский

Если ab = ac, то b = c.

LaTeX

$$$a \cdot b = a \cdot c \rightarrow b=c$$$

Lean4

@[to_additive]
theorem mul_left_cancel : a * b = a * c → b = c :=
  (IsLeftCancelMul.mul_left_cancel a ·)

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

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

Разделы

Аффилиация

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