cardPowDegree_apply — Mathlib

English

For any finite field Fq with decidable equality, and any polynomial p ∈ Fq[X], cardPowDegree p equals 0 if p = 0, otherwise q^{natDegree p}, where q = |Fq|.

Русский

Для конечного поля Fq с разрешимой эквивалентностью, и любого полинома p ∈ Fq[X], cardPowDegree p равно 0 при p = 0, иначе q^{natDegree p}, где q = |Fq|.

LaTeX

$$$ cardPowDegree\ p = \\begin{cases} 0, & p = 0 \\\\ (|Fq|)^{ natDegree\ p}, & p \\neq 0 \\end{cases} $$$

Lean4

theorem cardPowDegree_apply [DecidableEq Fq] (p : Fq[X]) :
    cardPowDegree p = if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ natDegree p :=
  by
  rw [cardPowDegree]
  dsimp
  convert rfl

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