feat(LinearAlgebra/Eigenspace/Matrix): a scalar is in the spectrum iff it's an eigenvalue#39635

SnirBroshi wants to merge 12 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

SnirBroshi:feature/matrix/mem-spectrum-iff-mulvecSnirBroshi/mathlib4:feature/matrix/mem-spectrum-iff-mulvecCopy head branch name to clipboard