eq_div_of_mul_eq

Mathlib.Algebra.Group.Units.Basic

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

English

Let α be a division monoid and let c be a unit in α. If a·c = b, then a = b / c.

Русский

Пусть α — делимый моноид, и c — обратимый элемент. Если a·c = b, то a = b / c.

LaTeX

$$$\forall a,b \in \alpha, \ c \in \alpha^{\times},\ a c = b \Rightarrow a = b / c$$$

Lean4

@[to_additive]
protected theorem eq_div_of_mul_eq (h : IsUnit c) : a * c = b → a = b / c :=
  h.eq_div_iff.2

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

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

Разделы

Аффилиация

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