frobenius_def

Mathlib.Algebra.CharP.Frobenius

URI: https://scilib.ai/kg/mathlib#frobenius_def

English

For a commutative semiring R of characteristic p, the Frobenius map sends x to x^p.

Русский

Для коммутативного полупривособр кольца R характериcтики p отображение Фробениуса отправляет x в x^p.

LaTeX

$$$\\\\text{frobenius } R\ \\\\ p\ (x) = x^p$$$

Lean4

theorem frobenius_def : frobenius R p x = x ^ p :=
  rfl

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

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

Разделы

Аффилиация

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