IsCycleOn — Mathlib

English

For finite β and a cycle f, f^n is a cycle iff n is coprime to orderOf f.

Русский

Для конечного β и цикла f, f^n является циклом тогда и только тогда, когда n взаимно просто с orderOf f.

LaTeX

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

Lean4

/-- A permutation is a cycle on `s` when any two points of `s` are related by repeated application
of the permutation. Note that this means the identity is a cycle of subsingleton sets. -/
def IsCycleOn (f : Perm α) (s : Set α) : Prop :=
  Set.BijOn f s s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → f.SameCycle x y

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