Theorem Mathlib.Tactic.Hessenberg.det_eq_sum_of_isUpperHessenberg

Modification history

2026-10-20 14:09
Mathlib/Tactic/Hessenberg/Charpoly.lean
feat(Tactic/Hessenberg): an algorithm that computes the characteristic polynomial of an Hessenberg matrix (#44431) …
Added Mathlib.Tactic.Hessenberg.det_eq_sum_of_isUpperHessenbergView on Github →