support_pow_coprime — Mathlib

English

Let σ be a permutation and n a natural number coprime to the order of σ. Then the support of σ^n is the same as the support of σ.

Русский

Пусть σ — перестановка, и n натуральное число, взаимно простое с порядком σ. Тогда поддержка σ^n совпадает с поддержкой σ.

LaTeX

$$$\\gcd(n, \\operatorname{order}(\\sigma)) = 1 \\Rightarrow \\operatorname{supp}(\\sigma^n) = \\operatorname{supp}(\\sigma).$$$

Lean4

theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) : (σ ^ n).support = σ.support :=
  by
  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
  exact le_antisymm (support_pow_le σ n) (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

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