inv_mul_eq_iff_eq_mul₀

Mathlib.Algebra.GroupWithZero.Units.Basic

URI: https://scilib.ai/kg/mathlib#inv_mul_eq_iff_eq_mul₀

English

If a ≠ 0, then a^{-1} · b = c iff b = a · c.

Русский

Если a ≠ 0, то a^{-1} · b = c эквивалентно b = a · c.

LaTeX

$$$\forall a,b,c\, \text{Ne}(a,0) \Rightarrow (a^{-1}\cdot b = c \iff b = a\cdot c)$$$

Lean4

theorem inv_mul_eq_iff_eq_mul₀ (ha : a ≠ 0) : a⁻¹ * b = c ↔ b = a * c :=
  ha.isUnit.inv_mul_eq_iff_eq_mul

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

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

Разделы

Аффилиация

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