subtypePerm_pow — Mathlib

English

The nth power of the subtype permutation equals the subtype permutation of the nth power of f with a corresponding power-adjusted predicate.

Русский

Степень n подтиповой перестановки равна перестановке от f в степени n с соответствующим преобразованием условия.

LaTeX

$$$$ (f.subtypePerm hf)^n = (f^n).subtypePerm (pow\_aux hf). $$$$

Lean4

@[simp]
theorem subtypePerm_pow (f : Perm α) (n : ℕ) (hf) :
    (f.subtypePerm hf : Perm { x // p x }) ^ n = (f ^ n).subtypePerm (pow_aux hf) := by
  induction n with
  | zero => simp
  | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]

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