eq_mul_of_inv_mul_eq₀

Mathlib.Algebra.GroupWithZero.Units.Basic

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

← MathLib Explorer

English

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

Русский

Пусть c ≠ 0 и b^{-1} a = c; тогда a = b c.

LaTeX

$$$ (c \\neq 0) \\land (b^{-1} a = c) \\Rightarrow a = b c $$$

Lean4

/-- A variant of `inv_mul_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable. -/
theorem eq_mul_of_inv_mul_eq₀ (hc : c ≠ 0) (h : b⁻¹ * a = c) : a = b * c :=
  (mul_eq_of_eq_inv_mul₀ hc h.symm).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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