Commit 2026-06-12 12:02 dc67aa92

View on Github →

feat: prove elementary spectral bound for Z-matrices (#40372) The intended application is to a Cartan matrix. The key idea is due to Suzuka Yu.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

deleted theorem Pi.abs_apply

deleted theorem Pi.abs_def

added theorem Pi.mabs_apply

added theorem Pi.mabs_def

added theorem Pi.mabs_eq_one

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.dot_mulVec_eq_sum_sum

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.hasEigenvalue_add'_iff

added theorem Module.End.hasEigenvalue_add_iff

added theorem Module.End.hasEigenvalue_neg_iff

added theorem Module.End.hasEigenvalue_sub'_iff

added theorem Module.End.hasEigenvalue_sub_iff

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

added theorem Module.End.HasEigenvalue.nonempty

Created Mathlib/LinearAlgebra/Matrix/ZMatrix.lean