toList_pow_apply_eq_rotate — Mathlib

English

For any p, x and n, the list produced by p^n equals the rotation by n of toList p x.

Русский

Для любого p, x и n список, получаемый из p^n, равен повороту на n от toList p x.

LaTeX

$$$$\forall {\alpha} [Fintype \alpha] [DecidableEq \alpha] {p : Equiv.Perm \alpha} {x : \alpha} {k : \mathbb{N}},\ \mathrm{toList}\ (p^{k})\ x = (\mathrm{toList}\ p\ x).\mathrm{rotate}\ k.$$$$

Lean4

theorem toList_pow_apply_eq_rotate (p : Perm α) (x : α) (k : ℕ) : p.toList ((p ^ k) x) = (p.toList x).rotate k :=
  by
  apply ext_getElem
  · simp only [length_toList, cycleOf_self_apply_pow, length_rotate]
  · intro n hn hn'
    rw [getElem_toList, getElem_rotate, getElem_toList, length_toList, pow_mod_card_support_cycleOf_self_apply, pow_add,
      mul_apply]

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