iterate_map_frobenius — Mathlib

English

For f : R →* R, p and n, f^[n] (frobenius R p x) = frobenius R p (f^[n] x).

Русский

Для f : R →* R, p и n выполняется: f^[n](frobenius R p x) = frobenius R p (f^[n] x).

LaTeX

$$$f^{[n]}\bigl(\mathrm{frobenius}_{R,p}(x)\bigr) = \mathrm{frobenius}_{R,p}\bigl(f^{[n]}(x)\bigr)$$$

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 _ _ _

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