Coefficient lists of characteristic polynomials from Hessenberg certificates

This file contains the computation of the coefficient list of the characteristic polynomial of a matrix literal, by the recurrence coeffHessCharpoly on the Hessenberg matrix of a Hessenberg.Similarity certificate of the matrix, with a proof that Matrix.charpoly is the polynomial with these coefficients.

Main definitions

• charpolyCoeffList: computes the coefficient list of the characteristic polynomial of a matrix literal with a proof that Matrix.charpoly is the polynomial with these coefficients.
• CoeffListResult: the coefficient list literal of a matrix literal, with its proof.
• inferCharpolyRing: checks that the characteristic polynomial computation can be performed on S.

structure Mathlib.Tactic.Hessenberg.CharpolyRing {u : Lean.Level} (S : Q(Type u)) : Type

The instances of a commutative ring S required to compute the characteristic polynomial.

• cS : Q(CommRing «$S»)

  The commutative ring instance on S.

• aS : Q(Algebra «$S» ℚ)

  ℚ is an S-algebra.

• fS : Q(FaithfulSMul «$S» ℚ)

  The algebra map S → ℚ is injective.

def Mathlib.Tactic.Hessenberg.inferCharpolyRing {u : Lean.Level} (S : Q(Type u)) (cS : Q(CommRing «$S»)) : Lean.MetaM (Except Lean.MessageData (CharpolyRing S))

Check that the commutative ring S has the instances available for the characteristic polynomial to be computed.

Equations

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

structure Mathlib.Tactic.Hessenberg.CoeffListResult {u : Lean.Level} {S : Q(Type u)} (cS : Q(CommRing «$S»)) {n : ℕ} (A : Q(Matrix (Fin «$n») (Fin «$n») «$S»)) : Type

The coefficient list of the characteristic polynomial of the matrix literal A and a proof that it's equal to Matrix.charpoly.

• cs : Q(List «$S»)

  The list literal of the coefficients, constant term first.

• charpoly_eq : Q(«$A».charpoly = Polynomial.ofCoeffList unknown_1)

  The proof that cs is the coefficient list of the characteristic polynomial.

def Mathlib.Tactic.Hessenberg.charpolyCoeffList {u : Lean.Level} (S : Q(Type u)) (r : CharpolyRing S) (n : ℕ) (A : Q(Matrix (Fin «$n») (Fin «$n») «$S»)) (entries : Array (Array Lean.Expr)) : Lean.MetaM (CoeffListResult r.cS A)

Compute the coefficient list of the characteristic polynomial of the matrix literal A with rows of entries entries with a proof that Matrix.charpoly A is the polynomial with these coefficients.

Equations

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