Theorem Matrix.mem_spectrum_iff_not_isUnit_eval_charpoly

Modification history

2026-05-23 12:03
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat(LinearAlgebra/Matrix/Charpoly/Eigs): generalize to `CommRing`s (#39601) …
Added Matrix.mem_spectrum_iff_not_isUnit_eval_charpolyView on Github →