@[instance 50]

instance Hex.DensePoly.instDivModLawsField {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : DivModLaws F

Executable long division is lawful over every lightweight field.

@[instance 50]

instance Hex.DensePoly.instGcdLawsField {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : GcdLaws F

Executable gcd and extended gcd are lawful over every lightweight field.

theorem Hex.DensePoly.xgcdLeftMonic_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : (p.xgcdLeftMonic q).gcd ∣ p ∧ (p.xgcdLeftMonic q).gcd ∣ q

The monic one-sided extended gcd's returned representative divides both inputs over a field.

theorem Hex.DensePoly.xgcdLeftMonic_bezout {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : ∃ (t : DensePoly F), (p.xgcdLeftMonic q).left * p + t * q = (p.xgcdLeftMonic q).gcd

The monic one-sided extended gcd preserves a Bezout identity, with the untracked right coefficient supplied existentially.

theorem Hex.DensePoly.size_eq_one_of_mul_eq_one {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) (h : p * q = 1) : p.size = 1

A polynomial admitting a multiplicative inverse has degree zero.

theorem Hex.DensePoly.dvd_of_mod_eq_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) (hmod : p % q = 0) : q ∣ p

Vanishing remainder supplies the quotient witness for divisibility.

theorem Hex.DensePoly.size_mul_field {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).size = p.size + q.size - 1

Over a field, nonzero polynomial products have the expected stored size.

theorem Hex.DensePoly.C_mul_C {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (a b : F) : C a * C b = C (a * b)

Multiplication of constant dense polynomials.

theorem Hex.DensePoly.size_lt_of_dvd_not_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {g p : DensePoly F} (hg : g ≠ 0) (hp : p ≠ 0) (hgp : g ∣ p) (hpg : ¬p ∣ g) : g.size < p.size

A proper polynomial divisor has strictly smaller stored size.

theorem Hex.DensePoly.monicize_gcd_size_lt_left {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) (hp : p ≠ 0) (hpdq : ¬p ∣ q) : (p.gcd q).monicize.size < p.size

The monic gcd is a strict divisor of a nonzero left input whenever the left input does not divide the right input.