Theorem Module.End.hasEigenvalue_add'_iff

Modification history

2026-06-12 12:02
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
feat: prove elementary spectral bound for Z-matrices (#40372) …
Added Module.End.hasEigenvalue_add'_iffView on Github →