def Hex.SparsePoly.divModMonic {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (s t : SparsePoly R) (ht : t.Monic) : SparsePoly R × SparsePoly R

Divide by a monic divisor, through the dense representation: two toDense and two ofDense conversions around DensePoly.divModMonic.

Equations

• s.divModMonic t ht = Prod.map Hex.SparsePoly.ofDense Hex.SparsePoly.ofDense (s.toDense.divModMonic t.toDense ⋯)

def Hex.SparsePoly.divMod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (s t : SparsePoly R) : SparsePoly R × SparsePoly R

Field-style division with remainder, through the dense representation.

Equations

• s.divMod t = Prod.map Hex.SparsePoly.ofDense Hex.SparsePoly.ofDense (s.toDense.divMod t.toDense)

def Hex.SparsePoly.gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (s t : SparsePoly R) : SparsePoly R

Euclidean gcd, through the dense representation: the dense cost at the degree, whatever the term count. A caller with a two-term input of degree 10^6 should expect this to cost what a dense gcd at degree 10^6 costs.

Equations

• s.gcd t = Hex.SparsePoly.ofDense (s.toDense.gcd t.toDense)

def Hex.SparsePoly.divExactMonic? {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (s t : SparsePoly R) (ht : t.Monic) : Option (SparsePoly R)

Exact division by a monic divisor: divModMonic with a zero-remainder test.

Equations

• s.divExactMonic? t ht = if (s.divModMonic t ht).snd = 0 then some (s.divModMonic t ht).fst else none

@[instance_reducible]

instance Hex.SparsePoly.instDivOfOneOfAddOfSubOfMul {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Div (SparsePoly R)

Equations

• Hex.SparsePoly.instDivOfOneOfAddOfSubOfMul = { div := fun (s t : Hex.SparsePoly R) => (s.divMod t).fst }

@[instance_reducible]

instance Hex.SparsePoly.instModOfOneOfAddOfSubOfMulOfDiv {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Mod (SparsePoly R)

Equations

• Hex.SparsePoly.instModOfOneOfAddOfSubOfMulOfDiv = { mod := fun (s t : Hex.SparsePoly R) => (s.divMod t).snd }

def Hex.SparsePoly.divMonomial? {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : Option (SparsePoly R)

Divide by the monomial x^e, the one division that stays sparse: none unless every stored exponent is at least e, and otherwise a subtraction on each exponent, O(s) with no filtering.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.SparsePoly.mulMonomial_divMonomial {C : Type u} [Lean.Grind.CommRing C] [DecidableEq C] {s q : SparsePoly C} {e : Nat} (h : s.divMonomial? e = some q) : mulMonomial e 1 q = s

Multiplying back by the monomial undoes divMonomial?.

theorem Hex.SparsePoly.dvd_of_toDense_dvd {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] {s t : SparsePoly S} (h : s.toDense ∣ t.toDense) : s ∣ t

Divisibility transports back from the dense representation.

theorem Hex.SparsePoly.toDense_dvd {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] {s t : SparsePoly S} (h : s ∣ t) : s.toDense ∣ t.toDense

Divisibility transports to the dense representation.

theorem Hex.SparsePoly.degree?_ofDense {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p : DensePoly S) : (ofDense p).degree? = p.degree?

The degree transports through ofDense.

theorem Hex.SparsePoly.divMod_spec {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.DivModLaws S] (s t : SparsePoly S) : (s.divMod t).fst * t + (s.divMod t).snd = s

The quotient and remainder reconstruct the dividend, transported from DensePoly.DivModLaws.

theorem Hex.SparsePoly.divMod_degree_lt {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.DivModLaws S] (s t : SparsePoly S) (h : 0 < t.natDegree) : (s.divMod t).snd.natDegree < t.natDegree

The remainder degree drops below a positive divisor degree, transported from DensePoly.DivModLaws.

theorem Hex.SparsePoly.divModMonic_spec {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.DivModLaws S] (s t : SparsePoly S) (ht : t.Monic) : (s.divModMonic t ht).fst * t + (s.divModMonic t ht).snd = s

The monic division satisfies the division identity. It carries [Div S] and [DivModLaws S] even though divModMonic does not, and that is not an oversight: the dense layer proves the monic identity by routing through divMod, so there is no unconditional dense statement to transport.

theorem Hex.SparsePoly.divExactMonic?_eq_some {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.DivModLaws S] {s t q : SparsePoly S} (ht : t.Monic) : s.divExactMonic? t ht = some q ↔ s = q * t

Exact monic division returns exactly the cofactors: the forward direction is the division identity with a zero remainder, the reverse is dense monic cancellation applied to the two reconstructions.

theorem Hex.SparsePoly.divExactMonic?_isSome {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.DivModLaws S] {s t : SparsePoly S} (ht : t.Monic) : (s.divExactMonic? t ht).isSome = true ↔ t ∣ s

Exact monic division succeeds exactly on multiples. A monic divisor is nonzero, so no t ≠ 0 side condition is needed.

theorem Hex.SparsePoly.gcd_dvd_left {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.GcdLaws S] (s t : SparsePoly S) : s.gcd t ∣ s

The gcd divides the left argument, transported from DensePoly.GcdLaws.

theorem Hex.SparsePoly.gcd_dvd_right {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.GcdLaws S] (s t : SparsePoly S) : s.gcd t ∣ t

The gcd divides the right argument.

theorem Hex.SparsePoly.dvd_gcd {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DensePoly.GcdLaws S] {d s t : SparsePoly S} (hs : d ∣ s) (ht : d ∣ t) : d ∣ s.gcd t

Common divisors divide the gcd.