def Hex.DensePoly.monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p : DensePoly F) : DensePoly F

Normalize a nonzero polynomial to leading coefficient 1; keep 0 fixed.

Equations

• p.monicize = if p.isZero = true then 0 else Hex.DensePoly.scale p.leadingCoeff⁻¹ p

@[simp]

theorem Hex.DensePoly.monicize_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : monicize 0 = 0

theorem Hex.DensePoly.size_monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p : DensePoly F) : p.monicize.size = p.size

Normalization preserves the stored size.

theorem Hex.DensePoly.monicize_monic {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p ≠ 0) : p.monicize.Monic

Normalizing a nonzero polynomial produces a monic polynomial.

theorem Hex.DensePoly.monicize_ne_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p ≠ 0) : p.monicize ≠ 0

Normalization of a nonzero polynomial is nonzero.

theorem Hex.DensePoly.xgcd_bezout_field {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : have r := p.xgcd q; r.left * p + r.right * q = r.gcd

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

theorem Hex.DensePoly.monicize_dvd_of_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {g p : DensePoly F} (hg : g ≠ 0) (hgp : g ∣ p) : g.monicize ∣ p

theorem Hex.DensePoly.divMod_mul_field {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (a q : DensePoly F) (hq : q ≠ 0) : ((a * q).divMod q).fst = a

theorem Hex.DensePoly.monic_ne_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p.Monic) : p ≠ 0

A monic polynomial over a nontrivial field is nonzero.

theorem Hex.DensePoly.mul_monic {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p q : DensePoly F} (hp : p.Monic) (hq : q.Monic) : (p * q).Monic

The product of two monic polynomials is monic.

theorem Hex.DensePoly.monic_dvd_antisymm {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p q : DensePoly F} (hp : p.Monic) (hq : q.Monic) (hpq : p ∣ q) (hqp : q ∣ p) : p = q

Two monic polynomials dividing one another are equal.

@[simp]

theorem Hex.DensePoly.monicize_monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p : DensePoly F) : p.monicize.monicize = p.monicize

theorem Hex.DensePoly.commonProduct_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (running incoming common left right bezoutLeft bezoutRight result r : DensePoly F) (hincomingNe : incoming ≠ 0) (hrunning : running = common * left) (hincoming : incoming = common * right) (hbezout : bezoutLeft * running + bezoutRight * incoming = common) (hresult : result = left * incoming) (hrunDvd : running ∣ r) (hinDvd : incoming ∣ r) : result ∣ r

A Bézout-certified product of coprime cofactors divides every common multiple of the two inputs.

def Hex.DensePoly.lcm {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : DensePoly F

The monic least common multiple of p and q, and 0 if either input is zero.

Equations

• p.lcm q = if (p.isZero || q.isZero) = true then 0 else have common := (p.gcd q).monicize; (p * (q.divMod common).fst).monicize

@[simp]

theorem Hex.DensePoly.lcm_zero_left {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (q : DensePoly F) : lcm 0 q = 0

@[simp]

theorem Hex.DensePoly.lcm_zero_right {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p : DensePoly F) : p.lcm 0 = 0

@[simp]

theorem Hex.DensePoly.lcm_zero_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : lcm 0 0 = 0

theorem Hex.DensePoly.dvd_lcm_left {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : p ∣ p.lcm q

The left input divides the least common multiple.

theorem Hex.DensePoly.dvd_lcm_right {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : q ∣ p.lcm q

The right input divides the least common multiple.

theorem Hex.DensePoly.lcm_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q r : DensePoly F) (hp : p ∣ r) (hq : q ∣ r) : p.lcm q ∣ r

The executable lcm divides every common multiple.

theorem Hex.DensePoly.lcm_normalized {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p q : DensePoly F) : (p.lcm q).monicize = p.lcm q

Least common multiples are normalized, including the zero cases.

theorem Hex.DensePoly.lcm_ne_zero {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p q : DensePoly F} (hp : p ≠ 0) (hq : q ≠ 0) : p.lcm q ≠ 0

An lcm of nonzero polynomials is nonzero.

theorem Hex.DensePoly.lcm_monic {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p q : DensePoly F} (hp : p ≠ 0) (hq : q ≠ 0) : (p.lcm q).Monic

An lcm of nonzero polynomials is monic.

def Hex.DensePoly.lcmList {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : List (DensePoly F) → DensePoly F

Fold least common multiples, using 1 for the empty family.

Equations

• Hex.DensePoly.lcmList = List.foldl Hex.DensePoly.lcm 1

@[simp]

theorem Hex.DensePoly.lcmList_nil {F : Type u} [Lean.Grind.Field F] [DecidableEq F] : lcmList [] = 1

theorem Hex.DensePoly.dvd_lcmList_of_mem {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} {xs : List (DensePoly F)} (hp : p ∈ xs) : p ∣ lcmList xs

A member of a list divides its folded least common multiple.

theorem Hex.DensePoly.lcmList_dvd {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (xs : List (DensePoly F)) (r : DensePoly F) (h : ∀ (p : DensePoly F), p ∈ xs → p ∣ r) : lcmList xs ∣ r

The folded LCM divides every common multiple of the list.

theorem Hex.DensePoly.lcmList_monic {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (xs : List (DensePoly F)) (h : ∀ (p : DensePoly F), p ∈ xs → p ≠ 0) : (lcmList xs).Monic

A list of nonzero polynomials has a monic folded LCM.