iterateFrobeniusEquiv_eq_pow — Mathlib

English

The inverse of the n-th Frobenius iterate equals the n-th power of the inverse Frobenius equivalence; i.e., (iterateFrobeniusEquiv R p n)^{-1} = ((frobeniusEquiv R p)^{-1})^n.

Русский

Обратный к n-й итерации Фробениуса равен n-й степени обратной эквивалентности Фробениуса: (iterateFrobeniusEquiv R p n)^{-1} = ((frobeniusEquiv R p)^{-1})^n.

LaTeX

$$$ (iterateFrobeniusEquiv\ R\ p\ n)^{-1} = (frobeniusEquiv\ R\ p)^{-1}^n. $$$

Lean4

theorem iterateFrobeniusEquiv_eq_pow : iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n :=
  DFunLike.ext' <| show _ = ⇑(RingAut.toPerm _ _) by rw [map_pow, Equiv.Perm.coe_pow]; exact (pow_iterate p n).symm

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