Theorem InnerProductSpace.Core.inner_self_ofReal_re

Modification history