inv_mul_eq_inv_mul_iff_mul_eq_mul

English

Let G be a commutative group. For all a, b, c, d ∈ G, a * b^{-1} = d^{-1} * c iff a * d = c * b.

Русский

Пусть G — коммутативная группа. Для любых a, b, c, d верно a b^{-1} = d^{-1} c ⇔ a d = c b.

LaTeX

$$$a \\cdot b^{-1} = d^{-1} \\cdot c \\iff a \\cdot d = c \\cdot b$$$

Lean4

@[to_additive]
theorem inv_mul_eq_inv_mul_iff_mul_eq_mul : b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b := by
  rw [← div_eq_inv_mul, ← div_eq_inv_mul, div_eq_div_iff_mul_eq_mul]

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