`BookProof.ChapterSpectralDirectSum.range_cyclicEmbedding` : LinearMap.range (cyclicEmbedding T hT xi).toLinearMap = cyclicSubspace T hT xi

Initializing...

`BookProof.ChapterSpectralDirectSum.range_cyclicEmbedding` : LinearMap.range (cyclicEmbedding T hT xi).toLinearMap = cyclicSubspace T hT xi · Prove2Me