28.3. Producing a factorization🔗

For a Polynomial ℤ input, factor_poly returns Hex.FactoredPoly: a scalar, a list of irreducible factors, and proofs that the scalar times their product is the input.

open Polynomial

noncomputable def facZ :=
  factor_poly ((X - 1) ^ 2 * (X ^ 2 + 1) * 6 : Polynomial ℤ)

example : facZ.scalar = 6 := rfl
example : facZ.factors.length = 3 := rfl

The tactic form introduces transparent local names and their proofs:

open Polynomial

example : True := by⊢ True
  factor_poly ((X - 1) * (X + 1) : Polynomial ℤ)scalar:ℤ := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).scalarfactors:List ℤ[X] := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).factorsfactors_mul:C scalar * factors.prod = (X - 1) * (X + 1)factors_irred:∀ q ∈ factors, Irreducible q⊢ True
  have _ := factors_mulscalar:ℤ := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).scalarfactors:List ℤ[X] := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).factorsfactors_mul:C scalar * factors.prod = (X - 1) * (X + 1)factors_irred:∀ q ∈ factors, Irreducible qx✝:C scalar * factors.prod = (X - 1) * (X + 1)⊢ True
  have _ := factors_irredscalar:ℤ := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).scalarfactors:List ℤ[X] := 
  (FactoredPoly.ofZ ((X - 1) * (X + 1)) (DensePoly.ofCoeffs #[-1, 0, 1]) 1
      [DensePoly.ofCoeffs #[1, 1], DensePoly.ofCoeffs #[-1, 1]]
      [(DensePoly.ofCoeffs #[1, 1], ZPoly.IrredWitness.linear), (DensePoly.ofCoeffs #[-1, 1], ZPoly.IrredWitness.linear)]
      [] ⋯ ⋯ ⋯).factorsfactors_mul:C scalar * factors.prod = (X - 1) * (X + 1)factors_irred:∀ q ∈ factors, Irreducible qx✝¹:C scalar * factors.prod = (X - 1) * (X + 1)x✝:∀ q ∈ factors, Irreducible q⊢ True
  trivialAll goals completed! 🐙

Over a prime field, the result has the analogous Hex.FpPoly.Factored type:

open Hex

local instance boundsFive : ZMod64.Bounds 5 :=
  ⟨by⊢ 0 < 5 decideAll goals completed! 🐙, by⊢ 5 < 2 ^ 31 decideAll goals completed! 🐙⟩

def fp : FpPoly 5 := #p[4, 0, 1]

def fpFactors : FpPoly.Factored fp :=
  factor_poly fp