@[reducible, inline]

abbrev Hex.SubresultantMinor.Square (R : Type u) (n : Nat) : Type u

A proof-only square coefficient family.

Equations

• Hex.SubresultantMinor.Square R n = (Fin n → Fin n → R)

def Hex.SubresultantMinor.skipIndex {n : Nat} (j : Fin (n + 1)) (k : Fin n) : Fin (n + 1)

Embed an index while skipping one position.

Equations

• Hex.SubresultantMinor.skipIndex j k = if h : ↑k < ↑j then ⟨↑k, ⋯⟩ else ⟨↑k + 1, ⋯⟩

def Hex.SubresultantMinor.deleteFirst {R : Type u} {n : Nat} (M : Square R (n + 1)) (j : Fin (n + 1)) : Square R n

Remove the first row and one selected column.

Equations

• Hex.SubresultantMinor.deleteFirst M j i k = M i.succ (Hex.SubresultantMinor.skipIndex j k)

def Hex.SubresultantMinor.sign {R : Type u} [Zero R] [One R] [Sub R] (j : Nat) : R

The alternating sign in a first-row Laplace expansion.

Equations

• Hex.SubresultantMinor.sign j = if j % 2 = 0 then 1 else 0 - 1

def Hex.SubresultantMinor.det {R : Type u} [Zero R] [One R] [Add R] [Sub R] [Mul R] {n : Nat} : Square R n → R

Local proof-only determinant, defined by first-row Laplace expansion. Its factorial recursion is not an executable resultant algorithm.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SubresultantMinor.det x_2 = 1

@[simp]

theorem Hex.SubresultantMinor.det_zero {R : Type u} [Zero R] [One R] [Add R] [Sub R] [Mul R] (M : Square R 0) : det M = 1

The empty local determinant is one.

theorem Hex.SubresultantMinor.Fraction.det_map {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] {n : Nat} (M : Square R n) : (det fun (i j : Fin n) => Fraction.ofCoeff (M i j)) = Fraction.ofCoeff (det M)

The coefficient embedding commutes with the local determinant.

def Hex.DensePoly.Subresultant.coeffInt {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (i : Int) : R

Read a coefficient at an integer index, returning zero below index zero.

Equations

• Hex.DensePoly.Subresultant.coeffInt p i = if i < 0 then 0 else p.coeff i.toNat

theorem Hex.DensePoly.Subresultant.coeffInt_ofNat {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (i : Nat) : coeffInt p (Int.ofNat i) = p.coeff i

A nonnegative integer-indexed lookup is the ordinary natural-indexed coefficient lookup. This explicit Int.ofNat form is useful for rewriting matrix indices before coercions have been normalized.

@[simp]

theorem Hex.DensePoly.Subresultant.coeffInt_natCast {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (i : Nat) : coeffInt p ↑i = p.coeff i

Coercion notation for the nonnegative integer-indexed coefficient law.

theorem Hex.DensePoly.Subresultant.coeffInt_add {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (t : Int) : coeffInt (p + q) t = coeffInt p t + coeffInt q t

Integer-indexed coefficient lookup distributes over polynomial addition.

def Hex.DensePoly.Subresultant.formalDegree {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : Nat

Default formal degree: zero and nonzero constants both have degree zero.

Equations

• Hex.DensePoly.Subresultant.formalDegree p = p.size - 1

def Hex.DensePoly.Subresultant.coeffMatrixAt {R : Type u} [Zero R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) : SubresultantMinor.Square R (df - J + (dg - J))

Scalar coefficient matrix at explicit formal degrees. Keeping the degree parameters separate makes coefficient embeddings definitionally dimension-preserving.

Equations

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

def Hex.DensePoly.Subresultant.coeffMinorAt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (df dg J l : Nat) (f g : DensePoly R) : R

One scalar coefficient minor at explicit formal degrees.

Equations

• Hex.DensePoly.Subresultant.coeffMinorAt df dg J l f g = Hex.SubresultantMinor.det (Hex.DensePoly.Subresultant.coeffMatrixAt df dg J l f g)

def Hex.DensePoly.Subresultant.coeffMinor {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J l : Nat) (f g : DensePoly R) : R

One scalar coefficient minor of the J-th generalized subresultant.

Equations

• Hex.DensePoly.Subresultant.coeffMinor J l f g = Hex.DensePoly.Subresultant.coeffMinorAt (Hex.DensePoly.Subresultant.formalDegree f) (Hex.DensePoly.Subresultant.formalDegree g) J l f g

def Hex.DensePoly.Subresultant.poly {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J : Nat) (f g : DensePoly R) : DensePoly R

Generalized Sylvester subresultant, assembled coefficientwise from scalar minors. Its degree is at most J.

Equations

• Hex.DensePoly.Subresultant.poly J f g = Hex.DensePoly.ofList (List.map (fun (l : Nat) => Hex.DensePoly.Subresultant.coeffMinor J l f g) (List.range (J + 1)))

@[simp]

theorem Hex.DensePoly.Subresultant.coeff_poly {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J : Nat) (f g : DensePoly R) (l : Nat) : (poly J f g).coeff l = if l < J + 1 then coeffMinor J l f g else Zero.zero

Coefficient l of the generalized subresultant is the corresponding scalar minor up to index J, and zero above.

theorem Hex.DensePoly.Subresultant.poly_size_le {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J : Nat) (f g : DensePoly R) : (poly J f g).size ≤ J + 1

The coefficient construction stores no terms above subresultant index J.

@[simp]

theorem Hex.DensePoly.Subresultant.Fraction.coeffInt_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) (i : Int) : coeffInt (Fraction.map p) i = Fraction.ofCoeff (coeffInt p i)

Integer-indexed coefficient lookup commutes with the fraction embedding.

@[simp]

theorem Hex.DensePoly.Subresultant.Fraction.formalDegree_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) : formalDegree (Fraction.map p) = formalDegree p

The fraction embedding preserves the default formal degree.

theorem Hex.DensePoly.Subresultant.Fraction.coeffMinorAt_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (df dg J l : Nat) (f g : DensePoly R) : coeffMinorAt df dg J l (Fraction.map f) (Fraction.map g) = Fraction.ofCoeff (coeffMinorAt df dg J l f g)

A coefficient minor at fixed formal degrees is preserved by the fraction embedding.

theorem Hex.DensePoly.Subresultant.Fraction.coeffMinor_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (J l : Nat) (f g : DensePoly R) : coeffMinor J l (Fraction.map f) (Fraction.map g) = Fraction.ofCoeff (coeffMinor J l f g)

Every generalized subresultant coefficient is preserved by the fraction embedding.

theorem Hex.DensePoly.Subresultant.Fraction.poly_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (J : Nat) (f g : DensePoly R) : poly J (Fraction.map f) (Fraction.map g) = Fraction.map (poly J f g)

Generalized Sylvester subresultants commute with the polynomial coefficient embedding. In particular, every coefficient of the fraction construction has an explicit base-ring image witness.

theorem Hex.DensePoly.Subresultant.Fraction.exists_coeff {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (J : Nat) (f g : DensePoly R) (l : Nat) : ∃ (c : R), Fraction.ofCoeff c = (poly J (Fraction.map f) (Fraction.map g)).coeff l

Coefficients of mapped generalized subresultants lie in the coefficient embedding image.