Commit 2025-07-27 15:47 0a739db8

feat(LinearAlgebra/Projection): lemmas on projections and invariant submodules (#25874) Proving some lemmas on invariant submodules, such as: For idempotent f and any operator T:

• range f is invariant under T iff f ∘ T ∘ f = T ∘ f
• ker f is invariant under T iff f ∘ T ∘ f = f ∘ T
• f and T commute iff both range f and ker f are invariant under T Added for both linear maps and continuous linear maps for convenience. Taken from leanprover-community/mathlib3#18289.