Theorem InnerProductSpace.Core.inner_self_nonneg

Modification history