pow_prime_eq_one_iff — Mathlib

English

For a permutation σ and a prime p, σ^p = 1 if and only if every cycle length in σ.cycleType equals p.

Русский

Для перестановки σ и простого p, σ^p = 1 тогда и только тогда, когда все длины циклов равны p.

LaTeX

$$$$\sigma^{p} = 1 \iff \forall c \in \sigma.\mathrm{cycleType}, c = p.$$$$

Lean4

theorem pow_prime_eq_one_iff {σ : Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)] : σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p :=
  by
  rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]
  apply forall_congr'
  exact fun c ↦
    ⟨fun hc h ↦ Or.resolve_left (hp.elim.eq_one_or_self_of_dvd c (hc h)) (Nat.ne_of_lt' (one_lt_of_mem_cycleType h)),
      fun hc h ↦ by rw [hc h]⟩

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