IsThreeCycle

Mathlib.GroupTheory.Perm.Cycle.Type

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.IsThreeCycle

English

A permutation is a three-cycle if and only if its cycle type is the singleton {3}.

Русский

Перестановка является трёхциклa, если и только если её тип цикла равен {3}.

LaTeX

$$$\IsThreeCycle(\sigma) \iff σ.cycleType = \{3\}$$$

Lean4

/-- A three-cycle is a cycle of length 3. -/
def IsThreeCycle [DecidableEq α] (σ : Perm α) : Prop :=
  σ.cycleType = { 3 }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru