Commit 2021-10-23 14:30 b877f6b8

chore(analysis/normed/group): generalize cauchy_seq.add (#9868) Also golf a few proofs.

deleted theorem cauchy_seq.add

modified theorem norm_eq_zero

modified theorem norm_le_zero_iff

modified theorem norm_pos_iff

added theorem cauchy_seq.add