Theorem Matrix.C_det_mul_charpoly_of_mul_eq_mul

Modification history

2026-10-06 16:05
Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
feat(LinearAlgebra/Matrix): upper Hessenberg matrices and Hessenberg similarity certificates (#43840) …
Added Matrix.C_det_mul_charpoly_of_mul_eq_mulView on Github →