mathlib

16d48d7e - feat(algebra/star/basic + analysis/normed_space/star/basic): add two eq_zero/ne_zero lemmas (#12412)