map_iterateFrobenius — Mathlib

English

For g : RingHom R S and n ∈ ℕ, g ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (g x).

Русский

Для RingHom g и n выполняется: g (iterateFrobenius R p n (x)) = iterateFrobenius S p n (g x).

LaTeX

$$$g\bigl((\mathrm{iterateFrobenius}_{R,p}(n))\,x\bigr) = \mathrm{iterateFrobenius}_{S,p}(n)\bigl(g(x)\bigr)$$$

Lean4

theorem map_iterateFrobenius (n : ℕ) : g (iterateFrobenius R p n x) = iterateFrobenius S p n (g x) :=
  g.toMonoidHom.map_iterateFrobenius p x n

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