Documentation

Mathlib.Algebra.Polynomial.Degree.CardPowDegree

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 #

Main results #

noncomputable def Polynomial.cardPowDegree {Fq : Type u_1} [Field Fq] [Fintype 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' := }
Instances For
    theorem Polynomial.cardPowDegree_apply {Fq : Type u_1} [Field Fq] [Fintype Fq] [DecidableEq Fq] (p : Polynomial Fq) :
    Polynomial.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] :
    Polynomial.cardPowDegree 0 = 0
    @[simp]
    theorem Polynomial.cardPowDegree_nonzero {Fq : Type u_1} [Field Fq] [Fintype Fq] (p : Polynomial Fq) (hp : p 0) :
    Polynomial.cardPowDegree p = (Fintype.card Fq) ^ p.natDegree
    theorem Polynomial.cardPowDegree_isEuclidean {Fq : Type u_1} [Field Fq] [Fintype Fq] :
    Polynomial.cardPowDegree.IsEuclidean