35.9. HexMvGcd: checked sparse multivariate gcds🔗

35.9.1. Introduction🔗

HexMvGcd supplies exact division, content, gcd, and square-free decomposition for Hex.MvPoly. The public gcd is canonical up to the coefficient-domain normalization convention, and every fast proposal is accepted only after replay by the common certificate checker.

The implementation is Mathlib-free. Integer inputs use heuristic and Brown modular producers before a deterministic subresultant fallback; rational and bounded prime-field inputs use the same checked boundary with the appropriate coefficient operations.

35.9.2. Exact division and normalization🔗

def

Hex.MvPoly.divMod.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp × Hex.MvPoly n R cmp
Hex.MvPoly.divMod.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp × Hex.MvPoly n R cmp

Division with remainder against one divisor. The zero-divisor branch is fixed as (0, f).

def

Hex.MvPoly.divExact?.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) : Option (Hex.MvPoly n R cmp)
Hex.MvPoly.divExact?.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) :
  Option (Hex.MvPoly n R cmp)

Exact quotient, rejecting a zero divisor before entering the fail-fast reduction loop.

theorem

Hex.MvPoly.divMod_spec.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) :
  f = (f.divMod g).fst * g + (f.divMod g).snd
Hex.MvPoly.divMod_spec.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  [Hex.IsMonomialOrder cmp]
  (f g : Hex.MvPoly n R cmp) :
  f =
    (f.divMod g).fst * g +
      (f.divMod g).snd

Division with remainder reconstructs its dividend.

theorem

Hex.MvPoly.eq_mul_of_divExact?_eq_some.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  {f g q : Hex.MvPoly n R cmp} (h : f.divExact? g = some q) : f = q * g
Hex.MvPoly.eq_mul_of_divExact?_eq_some.{u}
  {n : Nat} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  [Hex.IsMonomialOrder cmp]
  {f g q : Hex.MvPoly n R cmp}
  (h : f.divExact? g = some q) : f = q * g

Every quotient returned by the checked loop reconstructs the dividend. This direction needs no laws for GcdOps because each scalar quotient was validated by multiplication.

The division order is the polynomial's declared monomial order. Exact division returns none when the sparse remainder is nonzero; it never exposes a quotient that has not been checked against the original product.

def

Hex.MvPoly.content.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [Hex.GcdOps R]
  (p : Hex.MvPoly n R cmp) : R
Hex.MvPoly.content.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [Hex.GcdOps R]
  (p : Hex.MvPoly n R cmp) : R

Producer-free scalar content.

def

Hex.MvPoly.primPart.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp
Hex.MvPoly.primPart.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Divide every stored coefficient by scalar content, with primitive part zero for the zero polynomial.

def

Hex.MvPoly.polyNormalize.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.polyNormalize.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Hex.GcdOps R]
  [Hex.IsMonomialOrder cmp]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Canonical associate selected by the unit attached to the leading coefficient.

35.9.3. Certificates and the public gcd🔗

def

Hex.MvPoly.GcdCert.{u} (n : Nat) (R : Type u) [Lean.Grind.CommRing R]
  (cmp : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type u
Hex.MvPoly.GcdCert.{u} (n : Nat)
  (R : Type u) [Lean.Grind.CommRing R]
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type u

Public gcd certificate.

def

Hex.MvPoly.checkGcd.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (f h : Hex.MvPoly n R cmp) (cert : Hex.MvPoly.GcdCert n R cmp) : Bool
Hex.MvPoly.checkGcd.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.GcdOps R] [Hex.IsMonomialOrder cmp]
  (f h : Hex.MvPoly n R cmp)
  (cert : Hex.MvPoly.GcdCert n R cmp) :
  Bool

Replay a gcd candidate and its coprimality evidence.

theorem

Hex.MvPoly.checkGcd_sound.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.GcdOps R] [Hex.LawfulGcdOps R]
  [Hex.IsMonomialOrder cmp] {f h : Hex.MvPoly n R cmp}
  {cert : Hex.MvPoly.GcdCert n R cmp} (hc : f.checkGcd h cert = true) :
  f.CheckedGcdResult h cert.gcd cert.cofL cert.cofR
Hex.MvPoly.checkGcd_sound.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.GcdOps R] [Hex.LawfulGcdOps R]
  [Hex.IsMonomialOrder cmp]
  {f h : Hex.MvPoly n R cmp}
  {cert : Hex.MvPoly.GcdCert n R cmp}
  (hc : f.checkGcd h cert = true) :
  f.CheckedGcdResult h cert.gcd cert.cofL
    cert.cofR

Simultaneous checker soundness: exact cofactors, normalization, and coprimality.

def

Hex.MvPoly.gcdCert.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) : Hex.MvPoly.GcdCert n R cmp
Hex.MvPoly.gcdCert.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) :
  Hex.MvPoly.GcdCert n R cmp

Canonical checked gcd certificate.

def

Hex.MvPoly.gcd.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.gcd.{u} {n : Nat} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Canonically normalized gcd.

def

Hex.MvPoly.cofactors.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp × Hex.MvPoly n R cmp
Hex.MvPoly.cofactors.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp × Hex.MvPoly n R cmp

The exact left and right cofactors accompanying the canonical gcd.

The checker proves exact left and right cofactor identities and that the two remaining cofactors are coprime. The maximality theorem then gives the usual universal property.

theorem

Hex.MvPoly.gcd_dvd_left.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R] [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R] (f h : Hex.MvPoly n R cmp) : f.gcd h ∣ f
Hex.MvPoly.gcd_dvd_left.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) : f.gcd h ∣ f

The canonical gcd divides its left input.

theorem

Hex.MvPoly.gcd_dvd_right.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R] [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R] (f h : Hex.MvPoly n R cmp) : f.gcd h ∣ h
Hex.MvPoly.gcd_dvd_right.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h : Hex.MvPoly n R cmp) : f.gcd h ∣ h

The canonical gcd divides its right input.

theorem

Hex.MvPoly.dvd_gcd.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R] [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R] (f h d : Hex.MvPoly n R cmp) (hf : d ∣ f)
  (hh : d ∣ h) : d ∣ f.gcd h
Hex.MvPoly.dvd_gcd.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (f h d : Hex.MvPoly n R cmp)
  (hf : d ∣ f) (hh : d ∣ h) : d ∣ f.gcd h

Every common divisor divides the canonical gcd.

35.9.4. Named-variable content🔗

Multivariate factorization treats one variable as the current main variable. The recursive coefficient view supports content and primitive part in all other variables without changing the sparse ambient representation.

def

Hex.MvPoly.contentIn.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R] [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) : Hex.MvPoly n R cmp'
Hex.MvPoly.contentIn.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly n R cmp'

Content in a named main variable.

def

Hex.MvPoly.primPartIn.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R] [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) : Hex.MvPoly (n + 1) R cmp
Hex.MvPoly.primPartIn.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly (n + 1) R cmp

Primitive part in a named main variable.

theorem

Hex.MvPoly.contentIn_mul_primPartIn.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R] [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R] [Hex.MvPoly.GcdProducer R] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly.constIn i cmp' (Hex.MvPoly.contentIn i cmp' p) *
      Hex.MvPoly.primPartIn i cmp' p =
    p
Hex.MvPoly.contentIn_mul_primPartIn.{u}
  {n : Nat} {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly.constIn i cmp'
        (Hex.MvPoly.contentIn i cmp' p) *
      Hex.MvPoly.primPartIn i cmp' p =
    p

Named-variable content times primitive part reconstructs the input.

35.9.5. Square-free decomposition🔗

structure

Hex.MvPoly.SqfDecomp.{u} (n : Nat) (R : Type u) [Zero R]
  (cmp : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type u
Hex.MvPoly.SqfDecomp.{u} (n : Nat)
  (R : Type u) [Zero R]
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type u

Scalar content and the multiplicity-tagged square-free polynomial factors.

Constructor

Hex.MvPoly.SqfDecomp.mk.{u}

Fields

content : R

Scalar content separated from the polynomial factors.

factors : List (Hex.MvPoly.SqfFactor n R cmp)

Distinct square-free factors paired with their multiplicities.

def

Hex.MvPoly.sqfDecomp.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.BezoutOps R] [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp] [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) : Hex.MvPoly.SqfDecomp n R cmp
Hex.MvPoly.sqfDecomp.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp]
  [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly.SqfDecomp n R cmp

Characteristic-zero squarefree decomposition with recursive content and scalar content split off.

def

Hex.MvPoly.radical.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.BezoutOps R] [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp] [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.radical.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp]
  [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Product of the distinct polynomial factors; scalar content is omitted.

theorem

Hex.MvPoly.sqfDecomp_prod.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R] [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp] [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) :
  List.foldl (fun acc f => acc * f.factor ^ f.multiplicity)
      (Hex.MvPoly.C p.sqfDecomp.content) p.sqfDecomp.factors =
    p
Hex.MvPoly.sqfDecomp_prod.{u} {n : Nat}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp]
  [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) :
  List.foldl
      (fun acc f =>
        acc * f.factor ^ f.multiplicity)
      (Hex.MvPoly.C p.sqfDecomp.content)
      p.sqfDecomp.factors =
    p

Multiplying the scalar and factor powers reconstructs the input.

theorem

Hex.MvPoly.sqfDecomp_squarefree.{u} {n : Nat} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommRing R] [DecidableEq R] [BEq R]
  [LawfulBEq R] [Dvd R] [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R] [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp] [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp) (f : Hex.MvPoly.SqfFactor n R cmp) :
  f ∈ p.sqfDecomp.factors → f.factor.Squarefree
Hex.MvPoly.sqfDecomp_squarefree.{u}
  {n : Nat} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommRing R] [DecidableEq R]
  [BEq R] [LawfulBEq R] [Dvd R]
  [Hex.BezoutOps R] [Hex.LawfulGcdOps R]
  [Hex.LawfulBezoutOps R]
  [Hex.MvPoly.GcdProducer R]
  [Hex.IsMonomialOrder cmp]
  [Hex.MvPoly.NatNoZero R]
  (p : Hex.MvPoly n R cmp)
  (f : Hex.MvPoly.SqfFactor n R cmp) :
  f ∈ p.sqfDecomp.factors →
    f.factor.Squarefree

Every polynomial returned by square-free decomposition is square-free.

The decomposition records primitive square-free factors together with positive, increasing multiplicities. Its ordered product reconstructs the primitive part; scalar and monomial content remain explicit.

35.9.6. Cross-references🔗

HexMvPoly supplies the sparse representation and recursive coefficient views.
HexPolyZGcd supplies the univariate integer fallback and square-free base case.
HexMvHensel uses named-variable content and checked gcd certificates in its lifting contracts; HexMvFactor consumes the square-free split.