card_cycleType_pos — Mathlib

English

The cycle type has positive cardinality if and only if the permutation is not the identity.

Русский

Кардинал cycleType положителен тогда и только тогда, когда перестановка не тождественна.

LaTeX

$$$\forall \sigma : \mathrm{Perm}(\alpha), 0 < \sigma.\mathrmcycleType.card \iff \sigma \neq 1$$$

Lean4

theorem card_cycleType_pos {σ : Perm α} : 0 < Multiset.card σ.cycleType ↔ σ ≠ 1 :=
  pos_iff_ne_zero.trans card_cycleType_eq_zero.not

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