mathlib3

d7fcd8ca - chore(analysis/normed_space): remove 2 `norm_zero` lemmas (#3558)

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.