{d : ℕ} (S : Submodule ℂ E) [CompleteSpace S] (b : OrthonormalBasis (Fin d) ℂ S) : LinearMap.range (onbEmbedding S b : EuclideanSpace ℂ (Fin d) →ₗ[ℂ] E) = S

Initializing...

{d : ℕ} (S : Submodule ℂ E) [CompleteSpace S] (b : OrthonormalBasis (Fin d) ℂ S) : LinearMap.range (onbEmbedding S b : EuclideanSpace ℂ (Fin d) →ₗ[ℂ] E) = S · Prove2Me