English
n is in the cycle-type of σ if and only if σ can be decomposed as c τ with c, τ disjoint, c a cycle, and c.support.card = n.
Русский
n ∈ cycleType(σ) тогда и только тогда, когда σ можно разложить как c τ с раздельными компонентами, c — цикл, и c.support.card = n.
LaTeX
$$$$ n \in \mathrm{cycleType}(\sigma) \iff \exists c, \tau:\; \sigma = c \cdot \tau \land c \perp \tau \land \mathrm{IsCycle}(c) \land c.\mathrm{support}.card = n. $$$$
Lean4
theorem mem_cycleType_iff {n : ℕ} {σ : Perm α} :
n ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ c.support.card = n :=
by
constructor
· intro h
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
obtain ⟨c, cl, rfl⟩ := h
rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld
refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
· rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
· exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld
· rintro ⟨c, t, rfl, hd, hc, rfl⟩
simp [hd.cycleType_mul, hc.cycleType]
