Theorem inner_self_ofReal_norm

Modification history