Theorem inner_eq_sum_norm_sq_div_four

Modification history