inv_symm_left_iff — Mathlib

English

In any group, a semiconjugates y to x under a^{-1} if and only if a semiconjugates x to y under a; i.e. a^{-1} y = x a^{-1} ⇔ a x = y a.

Русский

Во всякой группе полусопряжение сохраняется после обращения к левому инверсному элементу: a^{-1} y = x a^{-1} ⇔ a x = y a.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by
  simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]

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