Theorem InnerProductSpace.Core.inner_smul_ofReal_right

Modification history