Theorem real_inner_self_eq_norm_mul_norm

Modification history