inv_inv_symm_iff — Mathlib

English

Let G be a division monoid. For all a, x, y in G, the condition that a^{-1} semiconjugates x^{-1} to y^{-1} is equivalent to a semiconjugating y to x; equivalently, a^{-1} x^{-1} = y^{-1} a^{-1} ⇔ a y = x a.

Русский

Пусть G — делительный моноид. Для любых a, x, y ∈ G равносильны условия: a^{-1} semiconjugates x^{-1} к y^{-1} и a semiconjugates y к x; то есть a^{-1} x^{-1} = y^{-1} a^{-1} ⇔ a y = x a.

LaTeX

$$$$\forall a,x,y \in G:\ a^{-1} x^{-1} = y^{-1} a^{-1} \iff a y = x a.$$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by
  simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]

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