isCycle_cycleRange

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.isCycle_cycleRange

← MathLib Explorer

English

If n>0 and i ≠ 0, then cycleRange(i) is a single cycle.

Русский

Если n>0 и i ≠ 0, то cycleRange(i) образует один цикл.

LaTeX

$$$\text{IsCycle}(\operatorname{cycleRange}(i))$$$

Lean4

theorem isCycle_cycleRange [NeZero n] (h0 : i ≠ 0) : IsCycle (cycleRange i) :=
  by
  obtain ⟨i, hi⟩ := i
  cases i
  · exact (h0 rfl).elim
  exact isCycle_finRotate.extendDomain _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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