isCycle_of_prime_order — Mathlib

English

If order of σ is prime and |σ|_support < 2·order(σ), then σ is a single cycle.

Русский

Если порядок σ прост и |спр| < 2·order(σ), тогда σ — единый цикл.

LaTeX

$$$$\text{If } \mathrm{orderOf}(\sigma) \text{ is prime and } |\sigma.\mathrm{support}| < 2\cdot \mathrm{orderOf}(\sigma), \ \sigma \text{ is a cycle}.$$$$

Lean4

theorem isCycle_of_prime_order {σ : Perm α} (h1 : (orderOf σ).Prime) (h2 : #σ.support < 2 * orderOf σ) : σ.IsCycle :=
  by
  obtain ⟨n, hn⟩ := cycleType_prime_order h1
  rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_lt_mul_iff_left₀ (orderOf_pos σ),
    Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2
  rw [← card_cycleType_eq_one, hn, card_replicate, h2]

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