Commit 2025-10-16 16:17 21259a98

View on Github →

feat(Analysis/InnerProductSpace): define the inner product on tensor products (#27228) This defines the inner product on tensor product spaces. Also defines OrthonormalBasis.tensorProduct. The implementation is based on here (by @jjaassoonn), which defines the inner product on real tensor product spaces. The exact same implementation also applies for the general case. Closes #6020

Estimated changes

added theorem Orthonormal.tmul
added theorem RCLike.inner_tmul_eq
added theorem TensorProduct.norm_lid
added theorem TensorProduct.norm_map