expand_card — Mathlib

English

Over the prime field Z/pZ, the Polynomial.expand map coincides with taking p-th powers.

Русский

В простом поле Z/pZ отображение Polynomial.expand совпадает с операцией взятия p-й степени.

LaTeX

$$$\\\\forall f \\\\in (\\\\mathbb{Z}/p\\\\mathbb{Z})[X], \\\\operatorname{expand}(\\\\mathbb{Z}/p\\\\mathbb{Z}, p, f) = f^{p}$$$

Lean4

theorem expand_card (f : Polynomial (ZMod p)) : expand (ZMod p) p f = f ^ p := by have h := FiniteField.expand_card f;
  rwa [ZMod.card p] at h

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