Commit 2025-08-29 09:37 e6f5b469
View on Github →feat(Analysis/InnerProductSpace/PiL2): (innerSL _ x).toMatrix and (toSpanSingleton _ x).toMatrix (#28344)
In bra-ket notation, this says that the matrix of |x⟩ given by basis b is the column matrix b.repr x, and that the matrix of ⟨x| given by orthonormal basis b is the row matrix star (b.repr x), where |x⟩ = toSpanSingleton _ x and ⟨x| = innerSL _ x
So then the matrix of a rank-one operator |x⟩⟨y| given by orthonormal basis b₂ and basis b is equal to vecMulVec (b.repr x) (star (b₂.repr y)).