conj_zpow — Mathlib

English

For all i ∈ ℤ and a, b in a group, the conjugate of b by a raised to the integer i equals the conjugate of b^i by a: (a b a^{-1})^i = a b^i a^{-1}.

Русский

Для любого i ∈ ℤ и элементов a, b в группе выполняется: (a b a^{-1})^i = a b^i a^{-1}.

LaTeX

$$$\forall i \in \mathbb{Z},\ \forall a,b \in \alpha,\ (a b a^{-1})^{i} = a b^{i} a^{-1}$$$

Lean4

@[simp]
theorem conj_zpow {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹ :=
  by
  cases i
  · simp
  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]

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