card_cycleType_eq_zero — Mathlib

English

For any permutation σ, the cardinality of its cycle type is zero iff σ is the identity.

Русский

КардиналcycleType(σ) равен 0 тогда и только тогда, когда σ — тождественная перестановка.

LaTeX

$$$\forall \sigma : \mathrm{Perm}(\alpha), \; \mathrm{Multiset}.card(\sigma.\mathrmcycleType) = 0 \iff \sigma = 1$$$

Lean4

theorem card_cycleType_eq_zero {σ : Perm α} : Multiset.card σ.cycleType = 0 ↔ σ = 1 := by
  rw [card_eq_zero, cycleType_eq_zero]

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