def Hex.SubresultantMinor.castSquare {R : Type u} {n m : Nat} (h : n = m) (M : Square R n) : Square R m

Reindex a square coefficient family along an equality of dimensions.

Equations

• Hex.SubresultantMinor.castSquare h M i j = M (Fin.cast ⋯ i) (Fin.cast ⋯ j)

@[simp]

theorem Hex.SubresultantMinor.castSquare_rfl {R : Type u} {n : Nat} (M : Square R n) : castSquare ⋯ M = M

Reindexing along a reflexive dimension equality changes nothing.

@[simp]

theorem Hex.SubresultantMinor.castSquare_apply {R : Type u} {n m : Nat} (h : n = m) (M : Square R n) (i j : Fin m) : castSquare h M i j = M (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Entrywise value of a dimension reindexing.

theorem Hex.SubresultantMinor.det_castSquare {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (h : n = m) (M : Square R n) : det (castSquare h M) = det M

Reindexing along a dimension equality does not change the local determinant.

def Hex.SubresultantMinor.swapAt {R : Type u} {n : Nat} (M : Square R n) (left : Nat) (h : left + 1 < n) : Square R n

Swap the columns at numeric positions left and left + 1.

Equations

• Hex.SubresultantMinor.swapAt M left h i j = if ↑j = left then M i ⟨left + 1, h⟩ else if ↑j = left + 1 then M i ⟨left, ⋯⟩ else M i j

@[simp]

theorem Hex.SubresultantMinor.swapAt_apply {R : Type u} {n : Nat} (M : Square R n) (left : Nat) (h : left + 1 < n) (i j : Fin n) : swapAt M left h i j = if ↑j = left then M i ⟨left + 1, h⟩ else if ↑j = left + 1 then M i ⟨left, ⋯⟩ else M i j

Entrywise value of a numeric adjacent-column swap.

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

A numeric adjacent-column swap negates the local determinant.

def Hex.SubresultantMinor.moveLeft {R : Type u} {n : Nat} (M : Square R n) (start count : Nat) : start + count < n → Square R n

Move the column at start + count to start, shifting the intervening columns one position to the right.

Equations

• Hex.SubresultantMinor.moveLeft M start 0 x_2 = M
• Hex.SubresultantMinor.moveLeft M start count.succ h = Hex.SubresultantMinor.moveLeft (Hex.SubresultantMinor.swapAt M (start + count) h) start count ⋯

theorem Hex.SubresultantMinor.moveLeft_apply {R : Type u} {n : Nat} (M : Square R n) (start count : Nat) (h : start + count < n) (i j : Fin n) : moveLeft M start count h i j = if ↑j = start then M i ⟨start + count, h⟩ else if start < ↑j ∧ ↑j ≤ start + count then M i ⟨↑j - 1, ⋯⟩ else M i j

Entrywise action of moving one column left across a consecutive range.

theorem Hex.SubresultantMinor.det_moveLeft {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (start count : Nat) (h : start + count < n) : det (moveLeft M start count h) = sign count * det M

Moving a column left across count positions contributes the parity sign of count.

def Hex.SubresultantMinor.rotateBlocks {R : Type u} {n : Nat} (M : Square R n) (start left right : Nat) : start + left + right ≤ n → Square R n

Rotate consecutive blocks of lengths left and right beginning at start, changing [A, B] to [B, A].

Equations

• Hex.SubresultantMinor.rotateBlocks M start left 0 x_2 = M
• Hex.SubresultantMinor.rotateBlocks M start left right.succ h = Hex.SubresultantMinor.rotateBlocks (Hex.SubresultantMinor.moveLeft M start left ⋯) (start + 1) left right ⋯

def Hex.SubresultantMinor.rotateIndex {n : Nat} (start left right : Nat) (h : start + left + right ≤ n) (j : Fin n) : Fin n

The column of the original matrix appearing at a given position after a consecutive-block rotation.

Equations

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

theorem Hex.SubresultantMinor.rotateBlocks_apply {R : Type u} {n : Nat} (M : Square R n) (start left right : Nat) (h : start + left + right ≤ n) (i j : Fin n) : rotateBlocks M start left right h i j = M i (rotateIndex start left right h j)

Entrywise action of rotating two consecutive column blocks.

theorem Hex.SubresultantMinor.det_rotateBlocks {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Square R n) (start left right : Nat) (h : start + left + right ≤ n) : det (rotateBlocks M start left right h) = sign (left * right) * det M

Rotating consecutive blocks contributes one adjacent swap for each pair of columns drawn from opposite blocks.

theorem Hex.DensePoly.Subresultant.coeffMatrixAt_rotate {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) : SubresultantMinor.castSquare ⋯ (SubresultantMinor.rotateBlocks (coeffMatrixAt df dg J l f g) 0 (dg - J) (df - J) ⋯) = coeffMatrixAt dg df J l g f

Rotating the two coefficient blocks of a generalized Sylvester matrix produces the matrix with its polynomial inputs exchanged.

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

Exchanging the inputs of a fixed-degree coefficient minor contributes the parity of the product of the two block lengths.

theorem Hex.DensePoly.Subresultant.coeffMinor_swap {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J l : Nat) (f g : DensePoly R) : coeffMinor J l f g = SubresultantMinor.sign ((formalDegree f - J) * (formalDegree g - J)) * coeffMinor J l g f

Exchanging the inputs of a generalized coefficient minor contributes the standard degree-product sign.

theorem Hex.DensePoly.Subresultant.poly_swap {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) : poly J f g = scale (SubresultantMinor.sign ((formalDegree f - J) * (formalDegree g - J))) (poly J g f)

Generalized Sylvester subresultants obey the standard input-swap sign law.