Commit 2025-07-28 23:36 3f4becef

feat(LinearAlgebra/Projection): define Submodule.IsCompl.projection (#27369) This defines Submodule.IsCompl.projection: the linear projection onto a subspace along its complement as a map from the full space to itself, as opposed to Submodule.linearProjOfIsCompl, which maps into the subtype. This version is important as it satisfies IsIdempotentElem. This is the linear map version of Submodule.starProjection when in a complete space where IsCompl U Uᗮ. An operator T is idempotent iff it equals the projection onto its range along its kernel (i.e., Submodule.IsCompl.projection where IsCompl (range T) (ker T)). An idempotent operator T is symmetric if and only if its range and kernel are pairwise orthogonal (a more general ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_orthogonal_range - so proof of this is golfed). Next pr: deprecate all instances of p.subtype.comp p.linearProjOfIsCompl q hpq and (p.linearProjOfIsCompl q hpq x : E) to hpq.projection and hpq.projection x respectively.