conj_pow — Mathlib

English

For all i ∈ ℕ and a, b in a group, conjugating b by a and then taking the i-th power equals conjugating 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{N},\ \forall a,b \in \alpha,\ (a b a^{-1})^{i} = a b^{i} a^{-1}$$$

Lean4

@[simp]
theorem conj_pow {i : ℕ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹ := by
  induction i with
  | zero => simp
  | succ i hi => simp [pow_succ, hi]

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