Commit 2020-07-26 07:03 d7fcd8ca

chore(analysis/normed_space): remove 2 norm_zero lemmas (#3558) We have a general norm_zero lemma and these lemmas are not used before we introduce normed_group instances.