isCycle_of_prime_order' — Mathlib

English

If a permutation σ has prime order and the size of the domain is less than twice that order, then σ is a single cycle.

Русский

Если перестановка σ имеет простый порядок и размер множества меньше чем удвоиный порядок, то σ — единичный цикл.

LaTeX

$$$(\\text{order}(\\sigma) \\text{ prime}) \\land (|\\alpha| < 2 \\cdot \\text{order}(\\sigma)) \\implies \\sigma \\text{ is a cycle}$$$

Lean4

theorem isCycle_of_prime_order' {σ : Perm α} (h1 : (orderOf σ).Prime) (h2 : Fintype.card α < 2 * orderOf σ) :
    σ.IsCycle := by classical exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

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