mul_inv_eq_iff_eq_mul₀ — Mathlib

English

Let b be a nonzero element. For all a, b, c in the group with zero, a multiplied by b inverse equals c if and only if a equals c times b.

Русский

Пусть b не равен нулю. Тогда для всех a, b, c из группы с нулём выполнено: a·b^{-1} = c тогда и только тогда, когда a = c·b.

LaTeX

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

Lean4

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

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