Lean: ker ⊕ range from disjointness + index 0 via quotient map injective⇒surjective

To prove IsCompl g.ker g.range for an operator g with finite-dim kernel, CoFG range and index 0 (e.g. g = (K - μ)^n at the stable ascent, K compact): (1) Disjointness: y = g x with g y = 0 means x ∈ ker g^(2n) = ker g^n (stability), so y = 0. Use Submodule.disjoint_def; rw [LinearMap.mem_ker, pow_add]; exact hy works because (f^n * f^n) x is defeq to f^n (f^n x). (2) Codisjointness: let q := g.range.mkQ ∘ₗ g.ker.subtype. q is injective by disjointness (Submodule.Quotient.mk_eq_zero). Index 0 gives finrank ker = finrank (X ⧸ range) after rw [LinearMap.index_eq_finrank_sub, sub_eq_zero, Nat.cast_inj] at hI. LinearMap.injective_iff_surjective_of_finrank_eq_finrank then gives surjectivity, and for any x, (Submodule.Quotient.eq _).1 hv.symm : x - v ∈ range splits x. This avoids proving descent separately.