pow_card_apply

Mathlib.GroupTheory.Perm.Cycle.Basic

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

English

If f is cycle-on s and a ∈ s, then (f^#s) a = a, i.e., cycling through all elements of s returns to a.

Русский

Если f — цикл на s и a ∈ s, то (f^|s|) a = a; полный цикл возвращает a.

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \land a \in s \Rightarrow (f^{|s|})a = a$$$

Lean4

theorem pow_card_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) : (f ^ #s) a = a :=
  (hf.pow_apply_eq ha).2 dvd_rfl

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

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

Разделы

Аффилиация

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