Fredholm property and index of $v$ when $(x,c)\mapsto v(x)+c$ is a bijection $E_0\times C\to F$

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$, let $E$, $F$ be Banach spaces over $\mathbb{K}$, and let $v:E\to F$ be a bounded linear map. Let $E_0\subseteq E$ be a linear subspace of finite codimension and $C\subseteq F$ a finite-dimensional linear subspace. If the map

is bijective, then $v$ is a Fredholm operator and

where $\operatorname{ind}v=\dim\operatorname{Ker}v-\dim(F/\operatorname{Im}v)$.

This gives a way to recognize a Fredholm operator, and to read off its index, from a bijective map obtained by restricting $v$ to a subspace of finite codimension and adding a finite-dimensional subspace of the target. It is reusable for statements about Fredholm operators near a given one and about perturbations.

Formalization Note. $E_0$ is an arbitrary Submodule 𝕜 E (no closedness assumption) with FiniteDimensional 𝕜 (E ⧸ E₀); $C$ is a Submodule 𝕜 F with FiniteDimensional 𝕜 C. The map $(x,c)\mapsto v(x)+c$ is (v.comp E₀.subtypeL).coprod C.subtypeL : E₀ × C →L[𝕜] F, and only its bijectivity as a function is assumed. Fredholm is Mathlib's ContinuousLinearMap.IsFredholm, and index is FredholmBanach.index (kernel minus cokernel, the opposite of Bourbaki's sign).