Absolute value on polynomials over a finite field.

Let 𝔽_q be a finite field of cardinality q, then the map sending a polynomial p to q ^ degree p (where q ^ degree 0 = 0) is an absolute value.

Main definitions

• Polynomial.cardPowDegree is an absolute value on 𝔽_q[t], the ring of polynomials over a finite field of cardinality q, mapping a polynomial p to q ^ degree p (where q ^ degree 0 = 0)

Main results

• Polynomial.cardPowDegree_isEuclidean: cardPowDegree respects the Euclidean domain structure on the ring of polynomials

noncomputable def Polynomial.cardPowDegree {Fq : Type u_1} [Field Fq] [Fintype Fq] : AbsoluteValue (Polynomial Fq) ℤ

cardPowDegree is the absolute value on 𝔽_q[t] sending f to q ^ degree f.

cardPowDegree 0 is defined to be 0.

Equations

• Polynomial.cardPowDegree = { toFun := fun (p : Polynomial Fq) => if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

theorem Polynomial.cardPowDegree_apply {Fq : Type u_1} [Field Fq] [Fintype Fq] [DecidableEq Fq] (p : Polynomial Fq) : cardPowDegree p = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

@[simp]

theorem Polynomial.cardPowDegree_zero {Fq : Type u_1} [Field Fq] [Fintype Fq] : cardPowDegree 0 = 0

@[simp]

theorem Polynomial.cardPowDegree_of_ne_zero {Fq : Type u_1} [Field Fq] [Fintype Fq] (p : Polynomial Fq) (hp : p ≠ 0) : cardPowDegree p = ↑(Fintype.card Fq) ^ p.natDegree

@[deprecated Polynomial.cardPowDegree_of_ne_zero (since := "2026-10-13")]

theorem Polynomial.cardPowDegree_nonzero {Fq : Type u_1} [Field Fq] [Fintype Fq] (p : Polynomial Fq) (hp : p ≠ 0) : cardPowDegree p = ↑(Fintype.card Fq) ^ p.natDegree

Alias of Polynomial.cardPowDegree_of_ne_zero.

theorem Polynomial.cardPowDegree_isEuclidean {Fq : Type u_1} [Field Fq] [Fintype Fq] : cardPowDegree.IsEuclidean