noncomputable def Hex.DensePoly.contentNat (p : DensePoly Int) : Nat

The nonnegative gcd of the coefficients of an integer polynomial.

Kernel-facing specification: one fold over the reference coefficient list. Compiled code runs the Array.foldl loop contentNatImpl via the @[csimp] proof contentNat_eq_impl.

Equations

• p.contentNat = List.foldl (fun (acc : Nat) (coeff : Int) => acc.gcd coeff.natAbs) 0 p.toList

def Hex.DensePoly.contentNatImpl (p : DensePoly Int) : Nat

Runtime implementation of contentNat: a direct Array.foldl with no intermediate list (value-equal to contentNat by contentNat_eq_impl, registered @[csimp]).

Equations

• p.contentNatImpl = Array.foldl (fun (acc : Nat) (coeff : Int) => acc.gcd coeff.natAbs) 0 p.toArray

theorem Hex.DensePoly.contentNat_eq_contentNatImpl (p : DensePoly Int) : p.contentNat = p.contentNatImpl

The reference contentNat and the Array.foldl runtime loop agree.

@[csimp]

theorem Hex.DensePoly.contentNat_eq_impl : contentNat = contentNatImpl

Register the Array.foldl loop as the compiled implementation of contentNat.

def Hex.DensePoly.content (p : DensePoly Int) : Int

The integer content of a polynomial. This is always nonnegative.

Equations

• p.content = Int.ofNat p.contentNat

noncomputable def Hex.DensePoly.primitivePart (p : DensePoly Int) : DensePoly Int

The primitive part obtained by dividing every coefficient by the content.

Kernel-facing specification: one map over the reference coefficient list. Compiled code runs the Array.map pass primitivePartImpl via the @[csimp] proof primitivePart_eq_impl.

Equations

• p.primitivePart = if p.contentNat = 0 then 0 else have c := Int.ofNat p.contentNat; Hex.DensePoly.ofList (List.map (fun (coeff : Int) => coeff / c) p.toList)

def Hex.DensePoly.primitivePartImpl (p : DensePoly Int) : DensePoly Int

Runtime implementation of primitivePart: one Array.map pass over the stored coefficients (value-equal to primitivePart by primitivePart_eq_impl, registered @[csimp]).

Equations

• p.primitivePartImpl = if p.contentNatImpl = 0 then 0 else have c := Int.ofNat p.contentNatImpl; Hex.DensePoly.ofCoeffs (Array.map (fun (coeff : Int) => coeff / c) p.toArray)

theorem Hex.DensePoly.primitivePart_eq_primitivePartImpl (p : DensePoly Int) : p.primitivePart = p.primitivePartImpl

The reference primitivePart and the Array.map runtime pass agree.

@[csimp]

theorem Hex.DensePoly.primitivePart_eq_impl : primitivePart = primitivePartImpl

Register the Array.map pass as the compiled implementation of primitivePart.

theorem Hex.DensePoly.content_dvd_coeff (p : DensePoly Int) (n : Nat) : p.content ∣ p.coeff n

The content of an integer polynomial divides every coefficient.

theorem Hex.DensePoly.dvd_content_of_nat_dvd_coeff (p : DensePoly Int) (d : Nat) (h : ∀ (n : Nat), ↑d ∣ p.coeff n) : ↑d ∣ p.content

If a natural number divides every integer coefficient, its integer cast divides the polynomial content.

theorem Hex.DensePoly.natCast_dvd_content_of_dvd_coeff (p : DensePoly Int) (d : Nat) (h : ∀ (n : Nat), ↑d ∣ p.coeff n) : ↑d ∣ p.content

If a natural number divides every coefficient, then it divides the content.

theorem Hex.DensePoly.nat_eq_one_of_content_eq_one_of_nat_dvd_coeff (p : DensePoly Int) (d : Nat) (hp : p.content = 1) (h : ∀ (n : Nat), ↑d ∣ p.coeff n) : d = 1

A natural number that divides every coefficient of a primitive integer polynomial must be 1.

theorem Hex.DensePoly.nat_dvd_of_scalar_mul_primitive_coeff_dvd (p : DensePoly Int) (d : Nat) (a : Int) (hp : p.content = 1) (h : ∀ (n : Nat), ↑d ∣ a * p.coeff n) : ↑d ∣ a

Scalar annihilator for primitive integer polynomials: if d divides every coefficient of a * p and p is primitive (content one), then d already divides a.

@[simp]

theorem Hex.DensePoly.content_mul_primitivePart (p : DensePoly Int) : scale p.content p.primitivePart = p

Scaling the primitive part by the content reconstructs the original integer polynomial.

@[simp]

theorem Hex.DensePoly.content_scale_neg_one (p : DensePoly Int) : (scale (-1) p).content = p.content

Multiplying an integer polynomial by -1 preserves its content.

@[simp]

theorem Hex.DensePoly.content_scale_int (c : Int) (p : DensePoly Int) : (scale c p).content = Int.ofNat c.natAbs * p.content

Content scales by the absolute value of the scaling integer.

theorem Hex.DensePoly.scale_neg_one_zero : scale (-1) 0 = 0

Scaling the zero integer polynomial by -1 is still zero.

@[simp]

theorem Hex.DensePoly.content_zero : content 0 = 0

The zero integer polynomial has content zero.

@[simp]

theorem Hex.DensePoly.content_C (c : Int) : (C c).content = Int.ofNat c.natAbs

The content of a constant integer polynomial is the absolute value of the constant.

@[simp]

theorem Hex.DensePoly.primitivePart_eq_zero_of_content_eq_zero (p : DensePoly Int) (h : p.content = 0) : p.primitivePart = 0

If an integer polynomial has zero content, its primitive part is zero.

@[simp]

theorem Hex.DensePoly.primitivePart_eq_self_of_content_eq_one (p : DensePoly Int) (h : p.content = 1) : p.primitivePart = p

A polynomial whose content is 1 equals its primitive part.

theorem Hex.DensePoly.primitivePart_primitive (p : DensePoly Int) (h : p.content ≠ 0) : p.primitivePart.content = 1

The primitive part of a polynomial with nonzero content has content 1.