{d : ℕ} {v : Fin d → E} (hv : Orthonormal ℂ v) : (adjoint (synthesis v)).comp (synthesis v) = ContinuousLinearMap.id ℂ (EuclideanSpace ℂ (Fin d))

Initializing...

{d : ℕ} {v : Fin d → E} (hv : Orthonormal ℂ v) : (adjoint (synthesis v)).comp (synthesis v) = ContinuousLinearMap.id ℂ (EuclideanSpace ℂ (Fin d)) · Prove2Me