Documentation

CompPoly.Univariate.Roots.RootProduct

Finite-Field Root Products #

Executable construction of gcd(p, X^q - X) as gcd(p, (X^q mod p) - (X mod p)), so large finite fields never materialize the dense polynomial X^q - X.

source
def CompPoly.CPolynomial.Raw.Roots.FiniteField.finiteFieldRootProductWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : MulContext F) (D : ModContext F) (ctx : Roots.FiniteField.FiniteFieldContext F) (p : Raw F) :
Raw F

Raw squarefree product of the linear factors of p whose roots lie in the field.

Instances For
    source
    def CompPoly.CPolynomial.Raw.Roots.FiniteField.finiteFieldRootProduct {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : Roots.FiniteField.FiniteFieldContext F) (p : Raw F) :
    Raw F

    Raw squarefree product using the default raw backends.

    Instances For
      source
      def CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) (p : CPolynomial F) :
      CPolynomial F

      The squarefree product of the linear factors of p whose roots lie in the field.

      Instances For
        source
        def CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProduct {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) (p : CPolynomial F) :
        CPolynomial F

        The squarefree product of the linear factors of p using the default raw backends.

        Instances For
          source
          theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith_toPoly_eq_normalize_gcd {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) {p : CPolynomial F} (hp : p ≠ 0) :
          have pMonic := p.monicNormalize; (finiteFieldRootProductWith M D ctx p).toPoly = normalize (EuclideanDomain.gcd pMonic.toPoly (ofArray (Raw.xPowSubXModWith M D ctx.q ↑pMonic)).toPoly)

          The finite-field root product agrees with the normalized Mathlib gcd of the monic input and its represented Frobenius witness.

          source
          theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith_dvd_frobenius_of_context {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) {p : CPolynomial F} (_hp : p ≠ 0) :
          (finiteFieldRootProductWith M D ctx p).toPoly ∣ Polynomial.X ^ ctx.q - Polynomial.X

          The finite-field root product divides the finite-field Frobenius polynomial.

          This is the modular-gcd bridge: the executable root product uses the congruent modular witness (X^q mod p) - (X mod p) instead of materializing X^q - X.

          source
          theorem CompPoly.CPolynomial.Roots.FiniteField.monicNormalize_ne_zero_of_ne_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} (hp : p ≠ 0) :
          p.monicNormalize ≠ 0

          Monic normalization preserves nonzeroness.

          source
          theorem CompPoly.CPolynomial.Roots.FiniteField.gcdMonic_ne_zero_of_left {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} (hp : p ≠ 0) :
          p.gcdMonic q ≠ 0

          The monic gcd of a nonzero left operand is nonzero.

          source
          theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith_ne_zero_of_ne_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) {p : CPolynomial F} (hp : p ≠ 0) :
          finiteFieldRootProductWith M D ctx p ≠ 0

          The finite-field root product of a nonzero polynomial is nonzero.