mul_right_cancel

Mathlib.Algebra.Group.Units.Basic

URI: https://scilib.ai/kg/mathlib#IsUnit.mul_right_cancel

English

If IsUnit b and a · b = c · b, then a = c.

Русский

Если IsUnit b и a·b = c·b, то a = c.

LaTeX

$$$ IsUnit\,b \rightarrow (a \cdot b = c \cdot b \Rightarrow a = c) $$$

Lean4

@[to_additive]
protected theorem mul_right_cancel (h : IsUnit b) : a * b = c * b → a = c :=
  h.mul_left_inj.1

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

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

Разделы

Аффилиация

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