Commit 2026-03-10 18:51 3e3898f0

View on Github →

feat(Analysis/Normed/Operator): prove the Fredholm alternative (#35048) This PR proves the Fredholm alternative for compact operators on a Banach space over a nontrivially normed field

depends on: #35001
depends on: #35052
depends on: #35226

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

added theorem ContinuousLinearMap.spectrum_eq

Created Mathlib/Analysis/Normed/Operator/FredholmAlternative.lean

added theorem IsCompactOperator.antilipschitz_of_not_hasEigenvalue

added theorem IsCompactOperator.hasEigenvalue_iff_mem_spectrum

added theorem IsCompactOperator.hasEigenvalue_or_mem_resolventSet