# mathlib3documentation

data.polynomial.degree.card_pow_degree

# Absolute value on polynomials over a finite field. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let Fq 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.card_pow_degree 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.card_pow_degree_is_euclidean: card_pow_degree respects the Euclidean domain structure on the ring of polynomials
noncomputable def polynomial.card_pow_degree {Fq : Type u_1} [field Fq] [fintype Fq] :

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

card_pow_degree 0 is defined to be 0.

Equations
theorem polynomial.card_pow_degree_apply {Fq : Type u_1} [field Fq] [fintype Fq] (p : polynomial Fq) :
= ite (p = 0) 0 ((fintype.card Fq) ^ p.nat_degree)
@[simp]
theorem polynomial.card_pow_degree_zero {Fq : Type u_1} [field Fq] [fintype Fq] :
@[simp]
theorem polynomial.card_pow_degree_nonzero {Fq : Type u_1} [field Fq] [fintype Fq] (p : polynomial Fq) (hp : p 0) :