pow_inv_comm — Mathlib

English

Let G be a group. For any a in G and m,n in natural numbers, (a^{-1})^{m} and a^{n} commute; equivalently (a^{-1})^{m} a^{n} = a^{n} (a^{-1})^{m}.

Русский

Пусть G — группа. Для любого a в G и натуральных m,n элементы (a^{-1})^{m} и a^{n} коммутируют; то есть (a^{-1})^{m} a^{n} = a^{n} (a^{-1})^{m}.

LaTeX

$$$\\forall a \\in G,\\ \forall m,n \\in \mathbb{N},\\ (a^{-1})^{m} a^{n} = a^{n} (a^{-1})^{m}$$$

Lean4

@[to_additive]
theorem pow_inv_comm (a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
  (Commute.refl a).inv_left.pow_pow _ _

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