Theorem IsCompactOperator.hasEigenvalue_or_mem_resolventSet

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