expand_card — Mathlib

English

Over a finite field K with q = |K|, the expansion operator satisfies expand_K(q)(f) = f^q for any polynomial f.

Русский

Для конечного поля K с q = |K| оператор расширения выполняет expand_K(q)(f) = f^q для любого многочлена f.

LaTeX

$$$\\operatorname{expand}_K(q)(f) = f^q \\quad( q=|K| )$$$

Lean4

theorem expand_card (f : K[X]) : expand K q f = f ^ q :=
  by
  obtain ⟨p, hp⟩ := CharP.exists K
  rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩
  haveI : Fact p.Prime := ⟨hp⟩
  dsimp at hn
  rw [hn, ← map_expand_pow_char, frobenius_pow hn, RingHom.one_def, map_id]

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