mathlib3 documentation

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 #

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.