isCycleOn_support_cycleOf

Mathlib.GroupTheory.Perm.Cycle.Factors

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

← MathLib Explorer

English

The permutation f is a single cycle on the support of its own cycle containing x.

Русский

Перестановка f образует едиичный цикл на поддержке своего цикла, содержащего x.

LaTeX

$$$f.\\\\IsCycleOn( (f.cycleOf x).\\\\support)$$$

Lean4

theorem isCycleOn_support_cycleOf [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
    f.IsCycleOn (f.cycleOf x).support :=
  isCycleOn_support_cycleOf_aux f x

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

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

Разделы

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

Аффилиация

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