pow_eq_one_iff'' — Mathlib

English

For a finite β and a cycle f, f^n = 1 iff for every moved point x (f x ≠ x), we have (f^n)x = x.

Русский

Для конечного β и цикла f, f^n = 1 эквивалентно тому, что для каждого перемещаемого x (f(x) ≠ x) имеет (f^n)x = x.

LaTeX

$$$\\forall f : \\mathrm{Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\Rightarrow \\forall n:\\mathbb{N},\\; f^n = 1 \\iff \\forall x, f x \\neq x \\rightarrow (f^n)x = x.$$$

Lean4

theorem pow_eq_one_iff'' [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∀ x, f x ≠ x → (f ^ n) x = x :=
  ⟨fun h _ hx => (hf.pow_eq_one_iff' hx).1 h, fun h =>
    let ⟨_, hx, _⟩ := id hf
    (hf.pow_eq_one_iff' hx).2 (h _ hx)⟩
    -- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption

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