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

source

noncomputable def polynomial.card_pow_degree {Fq : Type u_1} [field Fq] [fintype Fq] :

absolute_value (polynomial 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

polynomial.card_pow_degree = have card_pos : 0 < fintype.card Fq, from polynomial.card_pow_degree._proof_6, have pow_pos : ∀ (n : ℕ), 0 < ↑(fintype.card Fq) ^ n, from _, {to_mul_hom := {to_fun := λ (p : polynomial Fq), ite (p = 0) 0 (↑(fintype.card Fq) ^ p.nat_degree), map_mul' := _}, nonneg' := _, eq_zero' := _, add_le' := _}

source

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

⇑polynomial.card_pow_degree p = ite (p = 0) 0 (↑(fintype.card Fq) ^ p.nat_degree)

source

@[simp]

theorem polynomial.card_pow_degree_zero {Fq : Type u_1} [field Fq] [fintype Fq] :

⇑polynomial.card_pow_degree 0 = 0

source

@[simp]

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

⇑polynomial.card_pow_degree p = ↑(fintype.card Fq) ^ p.nat_degree

source

theorem polynomial.card_pow_degree_is_euclidean {Fq : Type u_1} [field Fq] [fintype Fq] :

polynomial.card_pow_degree.is_euclidean