Commit 2024-08-19 19:19 c4433ffe

feat: constructions of Hilbert C⋆-modules (#15765) In this file we define the following constructions of CStarModules where A denotes a C⋆-algebra. Note that for each type E, the instance is declared on the type synonym WithCStarModule E (with the notation C⋆ᵐᵒᵈ E), instead of on E itself.

1. A as a CStarModule over itself.
2. E × F as a CStarModule over A, when E and F are themselves CStarModules over A.
3. Π i : ι, E i as a CStarModule over A, when each E i is a CStarModule over A and ι is a Fintype.
4. E as a CStarModule over ℂ, when E is an InnerProductSpace over ℂ.