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 #
polynomial.card_pow_degree
is an absolute value on𝔽_q[t]
, the ring of polynomials over a finite field of cardinalityq
, mapping a polynomialp
toq ^ degree p
(whereq ^ 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] :
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' := _}
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)
@[simp]
@[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