cycleOf_apply

Mathlib.GroupTheory.Perm.Cycle.Factors

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

English

If two elements are in the same cycle (SameCycle f x y), then cycleOf f x y equals f y.

Русский

Если x и y лежат в одном и том же цикле перестановки, то cycleOf f x y = f y.

LaTeX

$$Theorem: cycleOf_apply [DecidableRel f.SameCycle] : SameCycle f x y → cycleOf f x y = f y$$

Lean4

theorem cycleOf_apply [DecidableRel f.SameCycle] : SameCycle f x y → cycleOf f x y = f y :=
  ofSubtype_apply_of_mem _

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

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

Разделы

Аффилиация

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