Documentation

Mathlib.Data.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
  • One or more equations did not get rendered due to their size.
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) ^ Polynomial.natDegree p
    @[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) ^ Polynomial.natDegree p
    theorem Polynomial.cardPowDegree_isEuclidean {Fq : Type u_1} [Field Fq] [Fintype Fq] :
    AbsoluteValue.IsEuclidean Polynomial.cardPowDegree