Mathlib: 1 - K Fredholm of index 0 for compact K, via finite-rank trick + homotopy

Mathlib (v4.35) has ContinuousLinearMap.IsFredholm, local constancy of the index (index_continuousOn_isFredholm) and the compact Fredholm alternative (IsCompactOperator.hasEigenvalue_or_mem_resolventSet), but not Riesz–Schauder. Cheap route: (1) ker(1-K) is finite-dim via hK.restrict' on the eigenspace + FiniteDimensional.of_isCompactOperator_id. (2) Finite codim by contradiction: if X/R is infinite-dim, pick finrank N independent vectors there (exists_linearIndependent_of_le_rank), lift by a right inverse of mkQ, and add F = φ ∘ P (P from ClosedComplemented.of_finiteDimensional); 1-(K-F) is injective, so bijective by the Fredholm alternative, so X/R is the image of N: contradiction. (3) Closed range comes for free: for Banach spaces, finite-dim complemented kernel + CoFG range ⟹ IsFredholm (restrict to a closed complement M, use closed_complemented_range_of_isCompl_of_ker_eq_bot, antilipschitz_of_injective_of_isClosed_range, IsClosedEmbedding.isFredholm, isFredholm_domRestrict_iff). (4) Index 0 and invariance under compact perturbation: isPreconnected_Icc.constant applied to t ↦ (T + (t:𝕜)•K).index, with the Fredholm property for each t from a quasi-inverse Q: Q∘(T+K) ≈ 1 + QK modulo finite rank (isFredholm_congr, FiniteRangeSetoid.equiv_iff_hasFiniteRange), then comp_iff_right.