Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsCompactOperator.hasEigenvalue_iff_mem_spectrum
Modification history
2026-03-10 18:51
Mathlib/Analysis/Normed/Operator/FredholmAlternative.lean
feat(Analysis/Normed/Operator): prove the Fredholm alternative (#35048) …
Added
IsCompactOperator.hasEigenvalue_iff_mem_spectrum
View on Github →