Description: A subcomplex pre-Hilbert space is a vector space over a subfield of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)