isCycle_of_prime_order'' — Mathlib

English

If the order of σ equals the size of α and that order is prime, then σ is a cycle.

Русский

Если порядок перестановки σ равен размеру α и этот порядок прост, то σ является циклом.

LaTeX

$$$(\\text{order}(\\sigma) = |\\alpha|) \\land (\\text{order}(\\sigma) \\text{ prime}) \\implies σ \\text{ is a cycle}$$$

Lean4

theorem isCycle_of_prime_order'' {σ : Perm α} (h1 : (Fintype.card α).Prime) (h2 : orderOf σ = Fintype.card α) :
    σ.IsCycle :=
  isCycle_of_prime_order' ((congr_arg Nat.Prime h2).mpr h1) <|
    by
    rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_iff_left₀ (orderOf_pos σ)]
    exact one_lt_two

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