Documentation

CompPoly.Fields.Binary.Tower.Support.DefiningPoly

Binary Tower Defining Polynomials #

Defining polynomials and basic degree lemmas used by the binary tower files.

source
noncomputable def definingPoly {F : Type u_1} [instField : Field F] (s : F) :
Polynomial F
Instances For
    source
    theorem degree_s_smul_X {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (Polynomial.C s * Polynomial.X).degree = 1
    source
    theorem degree_s_smul_X_add_1 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (Polynomial.C s * Polynomial.X + 1).degree = 1
    source
    theorem definingPoly_is_monic {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).Monic
    source
    theorem degree_definingPoly {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).degree = 2
    source
    theorem natDegree_definingPoly {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).natDegree = 2
    source
    theorem definingPoly_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    definingPoly s ≠ 0
    source
    theorem definingPoly_is_not_unit {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    ¬IsUnit (definingPoly s)
    source
    theorem definingPoly_coeffOf0 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).coeff 0 = 1
    source
    theorem definingPoly_coeffOf1 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).coeff 1 = s