def Hex.SubresultantMinor.setCol {R : Type u} {n : Nat} (M : Square R n) (dst : Fin n) (v : Fin n → R) : Square R n

Replace one column of a proof-only square coefficient family.

Equations

• Hex.SubresultantMinor.setCol M dst v i j = if j = dst then v i else M i j

@[simp]

theorem Hex.SubresultantMinor.setCol_apply {R : Type u} {n : Nat} (M : Square R n) (dst : Fin n) (v : Fin n → R) (i j : Fin n) : setCol M dst v i j = if j = dst then v i else M i j

Entrywise value of a column replacement.

@[simp]

theorem Hex.SubresultantMinor.setCol_self {R : Type u} {n : Nat} (M : Square R n) (dst : Fin n) : (setCol M dst fun (i : Fin n) => M i dst) = M

Replacing a column by itself changes nothing.

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

Swap two adjacent columns of a proof-only square coefficient family.

Equations

• Hex.SubresultantMinor.swapAdjacent M left i j = if j = left.castSucc then M i left.succ else if j = left.succ then M i left.castSucc else M i j

@[simp]

theorem Hex.SubresultantMinor.swapAdjacent_apply {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) (i j : Fin (n + 1)) : swapAdjacent M left i j = if j = left.castSucc then M i left.succ else if j = left.succ then M i left.castSucc else M i j

Entrywise value of an adjacent column swap.

theorem Hex.SubresultantMinor.swapAdjacent_left {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) (i : Fin (n + 1)) : swapAdjacent M left i left.castSucc = M i left.succ

After an adjacent swap, the left column reads the old right column. grind-only: simp derives this from swapAdjacent_apply.

theorem Hex.SubresultantMinor.swapAdjacent_right {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) (i : Fin (n + 1)) : swapAdjacent M left i left.succ = M i left.castSucc

After an adjacent swap, the right column reads the old left column. grind-only: simp derives this from swapAdjacent_apply.

theorem Hex.SubresultantMinor.swapAdjacent_of_ne {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) (i j : Fin (n + 1)) (hl : j ≠ left.castSucc) (hr : j ≠ left.succ) : swapAdjacent M left i j = M i j

Columns away from the swapped pair are untouched. grind-only: simp derives this from swapAdjacent_apply.

@[simp]

theorem Hex.SubresultantMinor.swapAdjacent_swapAdjacent {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) : swapAdjacent (swapAdjacent M left) left = M

Adjacent column swaps are involutive.

@[simp]

theorem Hex.SubresultantMinor.skipIndex_val_of_lt {n : Nat} (skip : Fin (n + 1)) (i : Fin n) (h : ↑i < ↑skip) : ↑(skipIndex skip i) = ↑i

Below the skipped position, the embedding preserves the numeric index.

@[simp]

theorem Hex.SubresultantMinor.skipIndex_val_of_not_lt {n : Nat} (skip : Fin (n + 1)) (i : Fin n) (h : ¬↑i < ↑skip) : ↑(skipIndex skip i) = ↑i + 1

From the skipped position on, the embedding shifts the numeric index up by one.

theorem Hex.SubresultantMinor.skipIndex_ne {n : Nat} (skip : Fin (n + 1)) (i : Fin n) : skipIndex skip i ≠ skip

A skipped-index embedding never returns the deleted position.

theorem Hex.SubresultantMinor.skipIndex_injective {n : Nat} (skip : Fin (n + 1)) : Function.Injective (skipIndex skip)

The skipped-index embedding is injective.

def Hex.SubresultantMinor.eraseIndex {n : Nat} (skip target : Fin (n + 1)) (h : target ≠ skip) : Fin n

Contract an index after deleting a distinct position.

Equations

• Hex.SubresultantMinor.eraseIndex skip target h = if hlt : ↑target < ↑skip then ⟨↑target, ⋯⟩ else ⟨↑target - 1, ⋯⟩

@[simp]

theorem Hex.SubresultantMinor.skipIndex_eraseIndex {n : Nat} (skip target : Fin (n + 1)) (h : target ≠ skip) : skipIndex skip (eraseIndex skip target h) = target

The skipped-index embedding undoes index contraction.

def Hex.SubresultantMinor.eraseAdjacent {n : Nat} (removed : Fin (n + 2)) (left : Fin (n + 1)) (hleft : removed ≠ left.castSucc) (hright : removed ≠ left.succ) : Fin n

The left position of an adjacent column pair after deleting a third column.

Equations

• Hex.SubresultantMinor.eraseAdjacent removed left hleft hright = if hlt : ↑removed < ↑left then ⟨↑left - 1, ⋯⟩ else ⟨↑left, ⋯⟩

@[simp]

theorem Hex.SubresultantMinor.skipIndex_eraseAdjacent_left {n : Nat} (removed : Fin (n + 2)) (left : Fin (n + 1)) (hleft : removed ≠ left.castSucc) (hright : removed ≠ left.succ) : skipIndex removed (eraseAdjacent removed left hleft hright).castSucc = left.castSucc

The contracted left column of an adjacent pair embeds back onto the original left column.

@[simp]

theorem Hex.SubresultantMinor.skipIndex_eraseAdjacent_right {n : Nat} (removed : Fin (n + 2)) (left : Fin (n + 1)) (hleft : removed ≠ left.castSucc) (hright : removed ≠ left.succ) : skipIndex removed (eraseAdjacent removed left hleft hright).succ = left.succ

The contracted right column of an adjacent pair embeds back onto the original right column.

theorem Hex.SubresultantMinor.deleteFirst_setCol_same {R : Type u} {n : Nat} (M : Square R (n + 1)) (dst : Fin (n + 1)) (v : Fin (n + 1) → R) : deleteFirst (setCol M dst v) dst = deleteFirst M dst

Deleting the replaced column removes the replacement.

theorem Hex.SubresultantMinor.deleteFirst_setCol_ne {R : Type u} {n : Nat} (M : Square R (n + 1)) (removed dst : Fin (n + 1)) (v : Fin (n + 1) → R) (h : dst ≠ removed) : deleteFirst (setCol M dst v) removed = setCol (deleteFirst M removed) (eraseIndex removed dst h) fun (i : Fin n) => v i.succ

Deleting another column preserves a replacement at the contracted index.

theorem Hex.SubresultantMinor.det_firstRow {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) (hzero : ∀ (j : Fin (n + 1)), 0 < ↑j → M ⟨0, ⋯⟩ j = 0) : det M = M ⟨0, ⋯⟩ ⟨0, ⋯⟩ * det (deleteFirst M ⟨0, ⋯⟩)

If the first row is supported only in its first column, the local determinant expands to that entry times the remaining first minor.

theorem Hex.SubresultantMinor.det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (dst : Fin n) (v w : Fin n → R) : det (setCol M dst fun (i : Fin n) => v i + w i) = det (setCol M dst v) + det (setCol M dst w)

The local Laplace determinant is additive in any replaced column.

theorem Hex.SubresultantMinor.det_setCol_smul {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (dst : Fin n) (c : R) (v : Fin n → R) : det (setCol M dst fun (i : Fin n) => c * v i) = c * det (setCol M dst v)

The local Laplace determinant is homogeneous in any replaced column.

theorem Hex.SubresultantMinor.det_setCol_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (dst : Fin n) : det (setCol M dst fun (x : Fin n) => 0) = 0

Replacing a column by zero makes the local determinant vanish.

def Hex.SubresultantMinor.toMatrix {R : Type u} {n : Nat} (M : Square R n) : Matrix R n n

Regard a proof-only square coefficient family as a Hex.Matrix.

Equations

• Hex.SubresultantMinor.toMatrix M = Hex.Matrix.ofFn M

theorem Hex.SubresultantMinor.toMatrix_get {R : Type u} {n : Nat} (M : Square R n) (i j : Fin n) : (toMatrix M)[i][j] = M i j

Entries are unchanged by the matrix view. Stated in the nested M[i][j] form like Matrix.getElem_ofFn, so it is grind-only: the simp-normal form of the left-hand side goes through Matrix.getRow.

theorem Hex.SubresultantMinor.det_toMatrix {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) : det M = (toMatrix M).det

The local first-row Laplace determinant agrees with the reusable Leibniz matrix determinant.

theorem Hex.SubresultantMinor.det_eq_zero_of_row_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (src dst : Fin n) (h : src ≠ dst) (hrow : ∀ (j : Fin n), M src j = M dst j) : det M = 0

A local determinant with two equal rows vanishes.

theorem Hex.SubresultantMinor.vector_eq_zero_of_mul_eq_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {n : Nat} (M : Square R n) (hn : 0 < n) (hdet : det M ≠ 0) (v : Vector R n) (hmul : toMatrix M * v = 0) (j : Fin n) : v[j] = 0

A square matrix with nonzero determinant has trivial right kernel over an exact-division domain.

def Hex.SubresultantMinor.lastCofactor {R : Type u} [Lean.Grind.CommRing R] {n : Nat} : Square R n → Fin n → R

The signed cofactor of a column along the final row.

Equations

• Hex.SubresultantMinor.lastCofactor x_3 j = j.elim0
• Hex.SubresultantMinor.lastCofactor M j = (Hex.SubresultantMinor.toMatrix M).cofactor (Fin.last n) j

theorem Hex.SubresultantMinor.lastCofactor_congr {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M N : Square R n) (j : Fin n) (h : ∀ (i k : Fin n), ↑i < n - 1 → M i k = N i k) : lastCofactor M j = lastCofactor N j

A final-row cofactor is independent of the entries in that final row.

theorem Hex.SubresultantMinor.det_lastCofactor {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) : det M = List.foldl (fun (acc : R) (j : Fin (n + 1)) => acc + M (Fin.last n) j * lastCofactor M j) 0 (List.finRange (n + 1))

Laplace expansion along the final row using lastCofactor.

theorem Hex.SubresultantMinor.det_lastCofactor_of_pos {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (hn : 0 < n) : det M = List.foldl (fun (acc : R) (j : Fin n) => acc + M ⟨n - 1, ⋯⟩ j * lastCofactor M j) 0 (List.finRange n)

Laplace expansion along the final row, stated for an arbitrary positive dimension.

theorem Hex.SubresultantMinor.det_lastRow_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) (hzero : ∀ (j : Fin (n + 1)), M (Fin.last n) j = 0) : det M = 0

A square family with zero final row has zero determinant.

theorem Hex.SubresultantMinor.det_lastRow_zero_of_pos {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (hn : 0 < n) (hzero : ∀ (j : Fin n), M ⟨n - 1, ⋯⟩ j = 0) : det M = 0

A positive-dimensional square family with zero final row has zero determinant.

def Hex.SubresultantMinor.scaleRange {R : Type u} [Mul R] {n : Nat} (M : Square R n) (start count : Nat) (c : R) : Square R n

Scale a consecutive range of columns.

Equations

• Hex.SubresultantMinor.scaleRange M start count c i j = if start ≤ ↑j ∧ ↑j < start + count then c * M i j else M i j

theorem Hex.SubresultantMinor.det_scaleRange {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (start count : Nat) (c : R) (hbound : start + count ≤ n) : det (scaleRange M start count c) = c ^ count * det M

Scaling count consecutive columns scales the determinant by c ^ count.

theorem Hex.SubresultantMinor.sign_succ {R : Type u} [Lean.Grind.CommRing R] (j : Nat) : sign (j + 1) = 0 - sign j

Consecutive Laplace signs are negatives.

theorem Hex.SubresultantMinor.sign_add {R : Type u} [Lean.Grind.CommRing R] (a b : Nat) : sign (a + b) = sign a * sign b

Alternating signs turn addition of exponents into multiplication.

theorem Hex.SubresultantMinor.sign_mul {R : Type u} [Lean.Grind.CommRing R] (a b : Nat) : sign (a * b) = sign a ^ b

A multiplied sign exponent is repeated multiplication of the sign.

theorem Hex.SubresultantMinor.sign_mul_self {R : Type u} [Lean.Grind.CommRing R] (n : Nat) : sign n * sign n = 1

Every alternating sign is its own multiplicative inverse.

theorem Hex.SubresultantMinor.sign_ne_zero {R : Type u} [Lean.Grind.CommRing R] (h1 : 1 ≠ 0) (n : Nat) : sign n ≠ 0

Every alternating sign is nonzero in a nontrivial ring.

theorem Hex.SubresultantMinor.deleteFirst_adjacent_eq {R : Type u} {n : Nat} (M : Square R (n + 2)) (left : Fin (n + 1)) (hcol : ∀ (i : Fin (n + 2)), M i left.castSucc = M i left.succ) : deleteFirst M left.castSucc = deleteFirst M left.succ

Deleting either member of an equal adjacent column pair gives the same minor.

theorem Hex.SubresultantMinor.det_eq_zero_of_adjacent_col_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) (left : Fin n) (hcol : ∀ (i : Fin (n + 1)), M i left.castSucc = M i left.succ) : det M = 0

The local determinant vanishes when two adjacent columns agree.

theorem Hex.SubresultantMinor.det_swapAdjacent {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) (left : Fin n) : det (swapAdjacent M left) = 0 - det M

Swapping two adjacent columns negates the local determinant.

def Hex.SubresultantMinor.applySwaps {R : Type u} {n : Nat} (M : Square R (n + 1)) (swaps : List (Fin n)) : Square R (n + 1)

Apply a sequence of adjacent column transpositions.

Equations

• Hex.SubresultantMinor.applySwaps M swaps = List.foldl Hex.SubresultantMinor.swapAdjacent M swaps

@[simp]

theorem Hex.SubresultantMinor.applySwaps_nil {R : Type u} {n : Nat} (M : Square R (n + 1)) : applySwaps M [] = M

The empty swap sequence acts as the identity.

@[simp]

theorem Hex.SubresultantMinor.applySwaps_cons {R : Type u} {n : Nat} (M : Square R (n + 1)) (left : Fin n) (swaps : List (Fin n)) : applySwaps M (left :: swaps) = applySwaps (swapAdjacent M left) swaps

A swap sequence acts head first.

@[simp]

theorem Hex.SubresultantMinor.applySwaps_append {R : Type u} {n : Nat} (M : Square R (n + 1)) (xs ys : List (Fin n)) : applySwaps M (xs ++ ys) = applySwaps (applySwaps M xs) ys

Concatenating swap sequences composes their column actions.

theorem Hex.SubresultantMinor.det_applySwaps {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R (n + 1)) (swaps : List (Fin n)) : det (applySwaps M swaps) = sign swaps.length * det M

A sequence of adjacent column transpositions multiplies the local determinant by its parity sign.

theorem Hex.SubresultantMinor.det_eq_zero_of_col_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (a b : Fin n) (hab : a ≠ b) (hcol : ∀ (i : Fin n), M i a = M i b) : det M = 0

The local determinant vanishes when any two distinct columns agree.

def Hex.SubresultantMinor.addCol {R : Type u} [Add R] [Mul R] {n : Nat} (M : Square R n) (src dst : Fin n) (c : R) : Square R n

Add a scalar multiple of one column to another.

Equations

• Hex.SubresultantMinor.addCol M src dst c = Hex.SubresultantMinor.setCol M dst fun (i : Fin n) => M i dst + c * M i src

@[simp]

theorem Hex.SubresultantMinor.addCol_apply {R : Type u} [Add R] [Mul R] {n : Nat} (M : Square R n) (src dst : Fin n) (c : R) (i j : Fin n) : addCol M src dst c i j = if j = dst then M i dst + c * M i src else M i j

Entrywise value of a scaled column addition.

theorem Hex.SubresultantMinor.det_addCol {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (src dst : Fin n) (c : R) (h : src ≠ dst) : det (addCol M src dst c) = det M

Adding a scalar multiple of one column to a distinct column preserves the local determinant.

@[simp]

theorem Hex.DensePoly.Subresultant.coeffInt_scale {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (c : R) (p : DensePoly R) (i : Int) : coeffInt (scale c p) i = c * coeffInt p i

Integer-indexed coefficient lookup commutes with scalar multiplication.

theorem Hex.DensePoly.Subresultant.coeffMatrixAt_scale_left {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (c : R) (f g : DensePoly R) : coeffMatrixAt df dg J l (scale c f) g = SubresultantMinor.scaleRange (coeffMatrixAt df dg J l f g) 0 (dg - J) c

Scaling the left polynomial scales exactly the left Sylvester block.

theorem Hex.DensePoly.Subresultant.coeffMatrixAt_scale_right {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (c : R) (f g : DensePoly R) : coeffMatrixAt df dg J l f (scale c g) = SubresultantMinor.scaleRange (coeffMatrixAt df dg J l f g) (dg - J) (df - J) c

Scaling the right polynomial scales exactly the right Sylvester block.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_scale_left {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (c : R) (f g : DensePoly R) : coeffMinorAt df dg J l (scale c f) g = c ^ (dg - J) * coeffMinorAt df dg J l f g

Fixed-degree coefficient minors are homogeneous in the left polynomial.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_scale_right {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (c : R) (f g : DensePoly R) : coeffMinorAt df dg J l f (scale c g) = c ^ (df - J) * coeffMinorAt df dg J l f g

Fixed-degree coefficient minors are homogeneous in the right polynomial.

theorem Hex.DensePoly.Subresultant.coeffMinor_scale_left {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {c : R} (hc : c ≠ 0) (J l : Nat) (f g : DensePoly R) : coeffMinor J l (scale c f) g = c ^ (formalDegree g - J) * coeffMinor J l f g

Generalized coefficient minors are homogeneous in the left polynomial.

theorem Hex.DensePoly.Subresultant.coeffMinor_scale_right {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {c : R} (hc : c ≠ 0) (J l : Nat) (f g : DensePoly R) : coeffMinor J l f (scale c g) = c ^ (formalDegree f - J) * coeffMinor J l f g

Generalized coefficient minors are homogeneous in the right polynomial.

theorem Hex.DensePoly.Subresultant.poly_scale_left {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {c : R} (hc : c ≠ 0) (J : Nat) (f g : DensePoly R) : poly J (scale c f) g = scale (c ^ (formalDegree g - J)) (poly J f g)

Generalized subresultants are homogeneous in the left polynomial.

theorem Hex.DensePoly.Subresultant.poly_scale_right {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {c : R} (hc : c ≠ 0) (J : Nat) (f g : DensePoly R) : poly J f (scale c g) = scale (c ^ (formalDegree f - J)) (poly J f g)

Generalized subresultants are homogeneous in the right polynomial.