Commit 2026-10-20 14:09 ab5a4bbf

feat(Tactic/Hessenberg): an algorithm that computes the characteristic polynomial of an Hessenberg matrix (#44431) add an algorithm that computes the characteristic polynomial of an upper Hessenberg matrix from the characteristic polynomials of its leading principal submatrices. Main definitions / theorems added:

• Matrix.toArray - constructs the array of entries of a matrix in row-major ordering.
• Mathlib.Tactic.Hessenberg.hessCharpoly - the Hessenberg characteristic polynomial algorithm in R[X]
• Mathlib.Tactic.Hessenberg.charpoly_eq_hessCharpoly - a proof that the Hessenberg characteristic algorithm computes Matrix.charpoly.
• Mathlib.Tactic.Hessenberg.coeffHessCharpoly - the Hessenberg characteristic polynomial algorithm stated for Polynomial coefficient lists (see #44430). This is more efficient for the kernel to check.