frobenius_zmod — Mathlib

English

For any polynomial f over ZMod p, Frobenius_p(f) equals expand_p(f).

Русский

Для любого многочлена f над ZMod p обозрение Фробениуса p-го порядка совпадает с expand_p(f).

LaTeX

$$frobenius_zmod (f) = expand p f$$

Lean4

theorem frobenius_zmod (f : MvPolynomial σ (ZMod p)) : frobenius _ p f = expand p f :=
  by
  apply induction_on f
  · intro a; rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
  · simp only [map_add]; intro _ _ hf hg; rw [hf, hg]
  · simp only [expand_X, map_mul]
    intro _ _ hf; rw [hf, frobenius_def]

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