cycleFactorsFinset_eq_empty_iff — Mathlib

English

The cycle factors finset is empty iff the permutation is the identity.

Русский

Цикловые факторы в конечном множителе пусты тогда и только тогда перестановка является единицей.

LaTeX

$$$cycleFactorsFinset(f) = \emptyset \iff f = 1$$$

Lean4

theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1 := by
  simpa [cycleFactorsFinset_eq_finset] using eq_comm

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