isCycle

Mathlib.GroupTheory.Perm.Cycle.Type

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

English

If a permutation σ is a three-cycle, then it is a single cycle (IsCycle).

Русский

Если σ — трёхцикл, то σ является одной циклической перестановкой.

LaTeX

$$$\IsThreeCycle(\sigma) \Rightarrow \IsCycle(\sigma)$$$

Lean4

theorem isCycle (h : IsThreeCycle σ) : IsCycle σ := by rw [← card_cycleType_eq_one, h.cycleType, card_singleton]

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

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

Разделы

Аффилиация

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