isCycle_formPerm

Mathlib.GroupTheory.Perm.Cycle.Concrete

URI: https://scilib.ai/kg/mathlib#Cycle.isCycle_formPerm

← MathLib Explorer

English

Given a nontrivial s, formPerm s h is a cycle.

Русский

Для ненулевого s, formPerm s h является циклом.

LaTeX

$$$IsCycle\\ (s.formPerm h)$$$

Lean4

theorem isCycle_formPerm (s : Cycle α) (h : Nodup s) (hn : Nontrivial s) : IsCycle (formPerm s h) :=
  by
  induction s using Quot.inductionOn
  exact List.isCycle_formPerm h (length_nontrivial hn)

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

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

Разделы

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

Аффилиация

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