inv_mul_eq_one

Mathlib.Algebra.Group.Units.Basic

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

English

If a is a unit, then a^{-1} · b = 1 if and only if a = b.

Русский

Если a — единица, тогда a^{-1} · b = 1 эквивалентно a = b.

LaTeX

$$IsUnit a → (a^{-1} * b = 1 \iff a = b)$$

Lean4

@[to_additive]
protected theorem inv_mul_eq_one (h : IsUnit a) : a⁻¹ * b = 1 ↔ a = b :=
  @Units.inv_mul_eq_one _ _ h.unit' _

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

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

Разделы

Аффилиация

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