theorem normalEquationPseudoinverse_isMoorePenroseInverse {𝓗 : Type u} {𝓚 : Type v} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] [NormedAddCommGroup 𝓚] [InnerProductSpace ℝ 𝓚] [CompleteSpace 𝓚] (T : 𝓗 →L[ℝ] 𝓚) [Fact (IsUnit (ContinuousLinearMap.adjoint T ∘SL T))] : IsMoorePenroseInverse T ((ContinuousLinearMap.adjoint T ∘SL T).inverse ∘SL ContinuousLinearMap.adjoint T)

Example 3.29: if T†T is invertible, then the operator (T†T)⁻¹ T† is the Moore-Penrose inverse of T.

instance instIsMoorePenroseInverseCompRealInverseCoeLinearIsometryEquivStarRingEndContinuousLinearMapIdAdjointOfFactIsUnit {𝓗 : Type u} {𝓚 : Type v} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] [NormedAddCommGroup 𝓚] [InnerProductSpace ℝ 𝓚] [CompleteSpace 𝓚] (T : 𝓗 →L[ℝ] 𝓚) [Fact (IsUnit (ContinuousLinearMap.adjoint T ∘SL T))] : IsMoorePenroseInverse T ((ContinuousLinearMap.adjoint T ∘SL T).inverse ∘SL ContinuousLinearMap.adjoint T)

The normal-equation pseudoinverse can be used through typeclass search when T†T is invertible.