eq_mul_inv_iff_mul_eq — Mathlib

English

For a, b in a monoid and c a unit, a = b·c^{-1} iff a·c = b.

Русский

Для элементов a,b в моноиде и единицы c верно: a = b c^{-1} тогда и только тогда a c = b.

LaTeX

$$$\forall a,b\in \alpha,\; \forall c\in \alpha^{\times}:\; a = b\,c^{-1} \iff a\,c = b$$$

Lean4

@[to_additive]
theorem eq_mul_inv_iff_mul_eq {a b : α} : a = b * ↑c⁻¹ ↔ a * c = b :=
  ⟨fun h => by rw [h, inv_mul_cancel_right], fun h => by rw [← h, mul_inv_cancel_right]⟩

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