# 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 #

• 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] :

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

cardPowDegree 0 is defined to be 0.

Instances For
theorem Polynomial.cardPowDegree_apply {Fq : Type u_1} [Field Fq] [Fintype Fq] (p : ) :
Polynomial.cardPowDegree p = if p = 0 then 0 else
@[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 : ) (hp : p 0) :
Polynomial.cardPowDegree p =
theorem Polynomial.cardPowDegree_isEuclidean {Fq : Type u_1} [Field Fq] [Fintype Fq] :
AbsoluteValue.IsEuclidean Polynomial.cardPowDegree