expand_zmod

Mathlib.FieldTheory.Finite.Polynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.expand_zmod

English

The expansion map on polynomials over ZMod p equals the p-th power map.

Русский

Расширение полиномов над ZMod p равно возведению в степень p.

LaTeX

$$expand p f = f^p$$

Lean4

theorem expand_zmod (f : MvPolynomial σ (ZMod p)) : expand p f = f ^ p :=
  (frobenius_zmod _).symm

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

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

Разделы

Аффилиация

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