cycleOf_apply_apply_pow_self

Mathlib.GroupTheory.Perm.Cycle.Factors

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

← MathLib Explorer

English

If f x ≠ x, then IsCycle (cycleOf f x).

Русский

Если f x ≠ x, то cycleOf f x образует цикл.

LaTeX

$$isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x)$$

Lean4

@[simp]
theorem cycleOf_apply_apply_pow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by convert cycleOf_apply_apply_zpow_self f x k using 1

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

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

Разделы

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

Аффилиация

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