inv_mul_eq_inv_mul_iff — Mathlib

English

For commutative monoid α and elements a,c and units b,d, b^{-1}a = d^{-1}c iff a d = c b.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem inv_mul_eq_inv_mul_iff : b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b := by
  rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]

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