zpow_apply_comm — Mathlib

English

Let σ be a permutation of α and m,n ∈ ℤ. Then for every x ∈ α, (σ^m)((σ^n)x) = (σ^n)((σ^m)x); i.e., powers of a permutation commute.

Русский

Пусть σ — перестановка α и m,n ∈ ℤ. Тогда для любого x ∈ α выполняется (σ^m)((σ^n)x) = (σ^n)((σ^m)x); то есть степени перестановки коммютируют.

LaTeX

$$$\\\\forall {α} (\\\\sigma : \\\\mathrm{Perm} \\\\alpha) (m n : \\\\mathbb{Z}) {x : \\\\alpha}, \\\\ (\\\\sigma ^ m) ((\\\\sigma ^ n) x) = (\\\\sigma ^ n) ((\\\\sigma ^ m) x)$$$

Lean4

theorem zpow_apply_comm {α : Type*} (σ : Perm α) (m n : ℤ) {x : α} : (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x) := by
  rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]

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