mathlib documentation

Absolute value on polynomials over a finite field. #

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 #

Main results #

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.

theorem polynomial.card_pow_degree_nonzero {Fq : Type u_1} [field Fq] [fintype Fq] (p : polynomial Fq) (hp : p 0) :