English
If order σ is prime, then cycle-type σ consists of blocks all equal to order(σ), i.e., cycleType(σ) = replicated blocks of order(σ).
Русский
Если порядок σ прост, цикл-тип σ состоит из блоков, все равны order(σ): cycleType(σ) = replication of order(σ).
LaTeX
$$$$\exists n,\; \sigma.\mathrm{cycleType} = \mathrm{Multiset.replicate}(n+1, \mathrm{orderOf}(\sigma)).$$$$
Lean4
theorem cycleType_prime_order {σ : Perm α} (hσ : (orderOf σ).Prime) :
∃ n : ℕ, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ) :=
by
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
· rw [tsub_add_cancel_of_le]
rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]
exact hσ.ne_one
· exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left (one_lt_of_mem_cycleType hn).ne'
