equivPair_tail_eq_inv_smul — Mathlib

English

For words over groups, the tail of equivPair equals the inverse-smul of w by the head.

Русский

Для слов над группами хвост equivPair равен inv-smul от w на голову.

LaTeX

$$$$ (equivPair i w).tail = (of (equivPair i w).head)^{-1} \\cdot w $$$$

Lean4

theorem equivPair_tail_eq_inv_smul {G : ι → Type*} [∀ i, Group (G i)] [∀ i, DecidableEq (G i)] {i} (w : Word G) :
    (equivPair i w).tail = (of (equivPair i w).head)⁻¹ • w :=
  Eq.symm <| inv_smul_eq_iff.2 (equivPair_head_smul_equivPair_tail w).symm

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