expand_char — Mathlib

English

The Frobenius-linearized expansion interacts with the Frobenius map: map (frobenius R p) (expand R p f) = f^p.

Русский

Расширение по Frobennia взаимодействует с отображением Фробениуса: map (frobenius R p) (expand R p f) = f^p.

LaTeX

$$$$\mathrm{map}(\mathrm{frobenius}\_R(p))\bigl(\mathrm{expand}_R(p,f)\bigr)=f^{p}$$$$

Lean4

theorem expand_char (f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p :=
  by
  refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_
  · rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
  · rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial, mul_pow, ← C.map_pow,
      frobenius_def]
    ring

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