map_iterateFrobenius

Mathlib.Algebra.CharP.Frobenius

URI: https://scilib.ai/kg/mathlib#MonoidHom.map_iterateFrobenius

English

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

Русский

Для f : R →* R и 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 map_iterateFrobenius (n : ℕ) : f (iterateFrobenius R p n x) = iterateFrobenius S p n (f x) := by
  simp [iterateFrobenius_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru