cycleOf_apply_apply_self

Mathlib.GroupTheory.Perm.Cycle.Factors

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

← MathLib Explorer

English

The cycleOf at x applied to x equals x; i.e., the cycle fixes its starting point.

Русский

Цикл cycleOf f x при применении к x возвращает x; цикл фиксирует начальную точку.

LaTeX

$$cycleOf f x x = f x$$

Lean4

@[simp]
theorem cycleOf_apply_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x (f x) = f (f x) := by
  convert cycleOf_apply_apply_pow_self f x 1 using 1

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

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

Разделы

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

Аффилиация

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