pow_eq_one_iff' — Mathlib

English

If there is a fixed distinguished point x with f x ≠ x, then f^n = 1 iff (f^n)x = x.

Русский

Если существует особая точка x с f(x) ≠ x, тогда f^n = 1 тогда, когда (f^n)x = x.

LaTeX

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

Lean4

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

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