eval_charpoly: characteristic polynomials of matrix literals

This module defines the norm_charpoly simproc and the eval_charpoly tactic, which evaluate the characteristic polynomial of a matrix literal over a commutative ring that embeds in ℚ (such as ℚ itself and ℤ) via a Matrix.Hessenberg.Similarity certificate checked by the kernel.

Implementation notes

The Hessenberg reduction algorithm used internally by the tactic divides by pivots, so the Matrix.Hessenberg.Similarity certificate is constructed over ℚ and the characteristic polynomial is pulled back to the coefficient ring R along the injective algebraMap R ℚ. Restricting to rings that embed in ℚ is a pragmatic choice made to support ℤ and ℚ first.

TODO

• Support ℤ directly by a fraction-free Hessenberg reduction.
• Support more general coefficient rings (such as ZMod p) by registering computational models per ring, as the Bareiss tactics do with bareiss_ext.

def norm_charpoly : Lean.Meta.Simp.Simproc

The norm_charpoly simproc evaluates the characteristic polynomial of matrix literals over a commutative ring α with [Algebra α ℚ] [FaithfulSMul α ℚ], such as ℚ and ℤ. The result is in the normal form of ring_nf. Terms that it cannot evaluate are skipped.

Equations

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

def evalCharpoly : Lean.ParserDescr

eval_charpoly evaluates the characteristic polynomial of matrix literals over a commutative ring α with [Algebra α ℚ] [FaithfulSMul α ℚ], such as ℚ and ℤ.

example : Matrix.charpoly (R := ℤ) !![1, 2; 3, 4] = X ^ 2 - 5 * X - 2 := by
  eval_charpoly

Terms skipped can be viewed by using set_option trace.Tactic.evalCharpoly true.

Equations

• evalCharpoly = Lean.ParserDescr.node `evalCharpoly 1024 (Lean.ParserDescr.nonReservedSymbol "eval_charpoly" false)