Documentation

CompPoly.Fields.Extension.Defs

Polynomial specifications for monic quotient presentations #

ExtensionParams.poly interprets the lower coefficient vector as the monic polynomial X^d + ∑ i, C lower[i] * X^i. The binomial specification is X^d - W; its conversion to an arbitrary monic presentation preserves that polynomial.

The carrier and executable operations are defined in Extension/Arithmetic.lean. These specifications do not certify the cardinality parameter or irreducibility. The quotient bridge and field laws are supplied separately in Extension/Bridge.lean and Extension/Field.lean.

source
noncomputable def CompPoly.Extension.ExtensionParams.poly {F : Type u_1} [Field F] (P : ExtensionParams F) :
Polynomial F

The monic defining polynomial X^d + ∑_{i < d} lower[i] · X^i. Part of the specification only; the computable arithmetic on Ext P never evaluates it.

Instances For
    source
    theorem CompPoly.Extension.ExtensionParams.degree_lower_lt {F : Type u_1} [Field F] (P : ExtensionParams F) :
    (∑ i : Fin P.d, Polynomial.C (P.lowerCoeff i) * Polynomial.X ^ ↑i).degree < ↑P.d

    The lower part of the modulus has degree strictly less than d.

    source
    theorem CompPoly.Extension.ExtensionParams.degree_poly {F : Type u_1} [Field F] (P : ExtensionParams F) :
    P.poly.degree = ↑P.d
    source
    theorem CompPoly.Extension.ExtensionParams.monic_poly {F : Type u_1} [Field F] (P : ExtensionParams F) :
    P.poly.Monic
    source
    @[simp]
    theorem CompPoly.Extension.ExtensionParams.natDegree_poly {F : Type u_1} [Field F] (P : ExtensionParams F) :
    P.poly.natDegree = P.d
    source
    noncomputable def CompPoly.Extension.BinomialParams.poly {F : Type u_1} [Field F] (P : BinomialParams F) :
    Polynomial F

    The defining polynomial X^d - W. Part of the specification only.

    Instances For
      source
      @[simp]
      theorem CompPoly.Extension.BinomialParams.natDegree_poly {F : Type u_1} [Field F] (P : BinomialParams F) :
      P.poly.natDegree = P.d
      source
      theorem CompPoly.Extension.BinomialParams.monic_poly {F : Type u_1} [Field F] (P : BinomialParams F) :
      P.poly.Monic
      source
      theorem CompPoly.Extension.BinomialParams.toExtensionParams_poly {F : Type u_1} [Field F] (P : BinomialParams F) :
      P.toExtensionParams.poly = P.poly

      The general-framework polynomial of a binomial agrees with X^d - W.