cycleType_eq_zero — Mathlib

English

For any permutation σ of α, σ.cycleType = 0 if and only if σ = 1 (the identity).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cycleType_eq_zero {σ : Perm α} : σ.cycleType = 0 ↔ σ = 1 := by
  simp [cycleType_def, cycleFactorsFinset_eq_empty_iff]

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