map_iterate_frobenius

Mathlib.Algebra.CharP.Frobenius

URI: https://scilib.ai/kg/mathlib#RingHom.map_iterate_frobenius

English

For g : RingHom R S and n ∈ ℕ, g((frobenius R p)^[n](x)) = (frobenius S p)^[n](g x).

Русский

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

LaTeX

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

Lean4

theorem map_iterate_frobenius (n : ℕ) : g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
  g.toMonoidHom.map_iterate_frobenius p x n

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

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

Разделы

Аффилиация

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