Theorem inner_self_eq_norm_sq_to_K

Modification history