def Hex.DensePoly.polyCRT {S : Type u_1} [Zero S] [DecidableEq S] [One S] [Add S] [Mul S] (a b u v s t : DensePoly S) : DensePoly S

Construct a polynomial with prescribed residues modulo coprime factors.

If s * a + t * b = 1, then polyCRT a b u v s t is congruent to u modulo a and to v modulo b; see polyCRT_congr_fst, polyCRT_congr_snd, polyCRT_mod_fst, and polyCRT_mod_snd.

Equations

• a.polyCRT b u v s t = u * t * b + v * s * a

def Hex.DensePoly.Congr {S : Type u_1} [Zero S] [DecidableEq S] [Add S] [Sub S] [Mul S] (p q m : DensePoly S) : Prop

Congr p q m means p and q differ by a multiple of m.

Equations

• p.Congr q m = (m ∣ p - q)

theorem Hex.DensePoly.congr_mod {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (p m : DensePoly S) : (p % m).Congr p m

Reduction modulo the modulus is congruent to the original polynomial over a lawful coefficient ring.

theorem Hex.DensePoly.mod_eq_mod_of_congr {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] {p q m : DensePoly S} : p.Congr q m → p % m = q % m

Congruent polynomials have the same canonical remainder once the divisor law package supplies the executable % invariants.

theorem Hex.DensePoly.dvd_of_mod_eq_mod {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] {p q m : DensePoly S} (h : p % m = q % m) : m ∣ p - q

Reverse direction of mod_eq_mod_of_congr: equal canonical remainders force the operands to be congruent modulo the divisor.

theorem Hex.DensePoly.congr_of_mod_eq_mod {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] {p q m : DensePoly S} (h : p % m = q % m) : p.Congr q m

Equal canonical remainders produce polynomial congruence modulo the divisor.

theorem Hex.DensePoly.mod_eq_mod_iff_congr {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] {p q m : DensePoly S} : p % m = q % m ↔ p.Congr q m

Polynomial congruence modulo m is equivalent to equality of canonical remainders.

theorem Hex.DensePoly.mod_add_mod {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (p q m : DensePoly S) : (p + q) % m = (p % m + q % m) % m

Reducing both summands before addition preserves the canonical remainder.

theorem Hex.DensePoly.mod_mul_mod {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (p q m : DensePoly S) : p * q % m = p % m * (q % m) % m

Reducing both factors before multiplication preserves the canonical remainder.

theorem Hex.DensePoly.polyCRT_congr_fst {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a b u v s t : DensePoly S) : s * a + t * b = 1 → (a.polyCRT b u v s t).Congr u a

The CRT witness is congruent to the prescribed first residue modulo a.

theorem Hex.DensePoly.polyCRT_congr_snd {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a b u v s t : DensePoly S) : s * a + t * b = 1 → (a.polyCRT b u v s t).Congr v b

The CRT witness is congruent to the prescribed second residue modulo b.

theorem Hex.DensePoly.polyCRT_modByMonic_fst {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (a b u v s t : DensePoly S) (ha : a.Monic) : s * a + t * b = 1 → (a.polyCRT b u v s t).modByMonic a ha = u.modByMonic a ha

The CRT witness reduces to the prescribed first residue modulo a via monic reduction.

theorem Hex.DensePoly.polyCRT_mod_fst {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (a b u v s t : DensePoly S) (ha : a.Monic) : s * a + t * b = 1 → a.polyCRT b u v s t % a = u % a

The CRT witness reduces to the prescribed first residue modulo a.

theorem Hex.DensePoly.polyCRT_modByMonic_snd {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (a b u v s t : DensePoly S) (hb : b.Monic) : s * a + t * b = 1 → (a.polyCRT b u v s t).modByMonic b hb = v.modByMonic b hb

The CRT witness reduces to the prescribed second residue modulo b via monic reduction.

theorem Hex.DensePoly.polyCRT_mod_snd {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (a b u v s t : DensePoly S) (hb : b.Monic) : s * a + t * b = 1 → a.polyCRT b u v s t % b = v % b

The CRT witness reduces to the prescribed second residue modulo b.

theorem Hex.DensePoly.coeff_mul_top_int (p q : DensePoly Int) (hp : 0 < p.size) (hq : 0 < q.size) : (p * q).coeff (p.size - 1 + (q.size - 1)) = p.coeff (p.size - 1) * q.coeff (q.size - 1)

The top coefficient of a product of nonzero integer polynomials is the product of their leading coefficients.

theorem Hex.DensePoly.mul_ne_zero_int (p q : DensePoly Int) (hp : p ≠ 0) (hq : q ≠ 0) : p * q ≠ 0

Integral domain property for integer polynomials.

theorem Hex.DensePoly.content_mul_of_primitive (p q : DensePoly Int) (hp : p.content = 1) (hq : q.content = 1) : (p * q).content = 1

Gauss's lemma for primitive integer polynomials: the product of two primitive polynomials is primitive.

theorem Hex.DensePoly.content_mul (p q : DensePoly Int) : (p * q).content = p.content * q.content

Gauss's lemma on content (multiplicative form): the content of a product of integer polynomials is the product of their contents. Strengthens content_mul_of_primitive to non-primitive inputs by decomposing each factor into its content and primitive part.

theorem Hex.DensePoly.scale_left_cancel {c : Int} (hc : c ≠ 0) {a b : DensePoly Int} (h : scale c a = scale c b) : a = b

Left-cancellation for integer scaling: a nonzero scalar can be cancelled from both sides of a scaled-polynomial equality.

theorem Hex.DensePoly.primitivePart_scale_of_primitive {c : Int} (hc : 0 < c) {r : DensePoly Int} (hr : r.content = 1) : (scale c r).primitivePart = r

Scaling a primitive polynomial by a positive integer leaves the primitive part unchanged: the scalar is absorbed entirely into the content.

theorem Hex.DensePoly.primitivePart_mul (p q : DensePoly Int) : (p * q).primitivePart = p.primitivePart * q.primitivePart

Gauss's lemma in primitive-part form: the primitive part of a product is the product of the primitive parts. The content scalars factor out via content_mul and content_mul_of_primitive, and the positive product scalar is absorbed by primitivePart_scale_of_primitive.

theorem Hex.DensePoly.dvd_contentNat_mul_of_dvd_mul_coeff (p q : DensePoly Int) (d : Nat) (h : ∀ (n : Nat), ↑d ∣ (p * q).coeff n) : d ∣ p.contentNat * q.contentNat

Gauss's lemma on content (divisibility form): if a natural number d divides every coefficient of p * q, then it divides contentNat p * contentNat q. This is the divisibility witness needed by the McCoy row construction used to obtain scalar annihilators.

theorem Hex.DensePoly.exists_scalar_annihilator_of_mul_coeff_dvd_of_exists_not_dvd_coeff (p q : DensePoly Int) (d : Nat) (hprod : ∀ (n : Nat), ↑d ∣ (p * q).coeff n) (hq : ∃ (n : Nat), ¬↑d ∣ q.coeff n) : ∃ (a : Int), ¬↑d ∣ a ∧ ∀ (i : Nat), ↑d ∣ a * p.coeff i

Public McCoy scalar-annihilator wrapper for integer dense polynomials.

If d divides every coefficient of p * q and some coefficient of q is not divisible by d, then a non-d-divisible scalar annihilates all coefficients of p modulo d.

theorem Hex.DensePoly.coeff_dvd_of_primitive_mul_coeff_dvd (p q : DensePoly Int) (d : Nat) (hp : p.content = 1) (hprod : ∀ (n : Nat), ↑d ∣ (p * q).coeff n) (n : Nat) : ↑d ∣ q.coeff n

Coefficient divisibility transfer for primitive products: if p is primitive (content one) and a natural number d divides every coefficient of p * q, then d divides every coefficient of q. Proved by contradiction using the McCoy scalar annihilator exists_scalar_annihilator_of_mul_coeff_dvd_of_exists_not_dvd_coeff and the primitive scalar annihilator nat_dvd_of_scalar_mul_primitive_coeff_dvd.