map_frobenius

Mathlib.Algebra.CharP.Frobenius

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

English

For a MonoidHom f, the Frobenius endomorphism commutes with f: f (frobenius R p x) = frobenius S p (f x).

Русский

Для моноидного гомоморфизма f Фробениус-компонента совместима: f(frobenius_R_p(x)) = frobenius_S_p(f(x)).

LaTeX

$$$f(\mathrm{frobenius}_{R,p}(x)) = \mathrm{frobenius}_{S,p}(f(x))$$$

Lean4

theorem map_frobenius : f (frobenius R p x) = frobenius S p (f x) :=
  map_pow f x p

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

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

Разделы

Аффилиация

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