eq_inv_mul_iff_mul_eq₀

Mathlib.Algebra.GroupWithZero.Units.Basic

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

English

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

Русский

Если b ≠ 0, то a = b^{-1} · c тогда и только тогда, когда b · a = c.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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