card_cycleType_eq_one — Mathlib

English

Let σ be a permutation of a finite set α. The cycle-type multiset has exactly one element if and only if σ is a single cycle.

Русский

Пусть σ — перестановка на конечном множестве α. Мультимножество типа цикла имеет ровно один элемент тогда и только тогда σ образует один цикл.

LaTeX

$$$$\#(\sigma.\mathrm{cycleType}) = 1 \iff \sigma \text{ is a cycle}.$$$$

Lean4

theorem card_cycleType_eq_one {σ : Perm α} : Multiset.card σ.cycleType = 1 ↔ σ.IsCycle :=
  by
  rw [card_eq_one]
  simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
    cycleFactorsFinset_eq_singleton_iff]
  grind

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