div_eq_of_eq_mul

Mathlib.Algebra.Group.Units.Basic

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

English

If b is a unit and a = c · b, then a / b = c.

Русский

Если b — единица и a = c · b, то a / b = c.

LaTeX

$$IsUnit b → (a = c * b → a / b = c)$$

Lean4

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

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

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

Разделы

Аффилиация

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