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_spectrumView on Github →