Commit 2026-05-23 12:03 9eb40b41

View on Github →

feat(LinearAlgebra/Matrix/Charpoly/Eigs): generalize to CommRings (#39601) Also adds r ∈ spectrum R B ↔ ¬IsUnit (B.charpoly.eval r) which is the ring version of r ∈ spectrum K A ↔ A.charpoly.IsRoot r.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

modified theorem Matrix.det_eq_prod_roots_charpoly_of_splits

added theorem Matrix.mem_spectrum_iff_not_isUnit_eval_charpoly

modified theorem Matrix.mem_spectrum_of_isRoot_charpoly

modified theorem Matrix.trace_eq_sum_roots_charpoly_of_splits