eq_inv_mul_iff_mul_eq

Mathlib.Algebra.Group.Units.Basic

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

English

If c is a unit, then a = b⁻¹·c iff b·a = c.

Русский

Если c — единичный элемент, то a = b⁻¹·c эквивалентно b·a = c.

LaTeX

$$$$IsUnit(b) \Rightarrow (a = b^{-1}\cdot c \iff b\cdot a = c).$$$$

Lean4

@[to_additive]
protected theorem eq_inv_mul_iff_mul_eq (h : IsUnit b) : a = b⁻¹ * c ↔ b * a = c :=
  h.unit'.eq_inv_mul_iff_mul_eq

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

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

Разделы

Аффилиация

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