inv_right_iff — Mathlib

English

In a group, SemiconjBy a x^{-1} y^{-1} is equivalent to SemiconjBy a x y; i.e., a x^{-1} = y^{-1} a ⇔ a x = y a.

Русский

В группе SemiconjBy a x^{-1} y^{-1} эквивалентно SemiconjBy a x y; то есть a x^{-1} = y^{-1} a ⇔ a x = y a.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by rw [← inv_symm_left_iff, inv_inv_symm_iff]

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