iterate_map_frobenius — Mathlib

English

For f : RingHom R S and n ∈ ℕ, (iterateFrobenius R p n) followed by f equals the corresponding iterate on S after f.

Русский

Для f : RingHom R S и n выполняется соответствующее сохранение итераций Фробениуса.

LaTeX

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

Lean4

theorem iterate_map_frobenius (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
    f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
  iterate_map_pow f _ _ _

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