mathlib

8e8c7fd5 - feat(analysis/normed_space/star/basic): in a C⋆-ring `star x * x = 0 ↔ x = 0` (#16672)

feat(analysis/normed_space/star/basic): in a C⋆-ring `star x * x = 0 ↔ x = 0` (#16672) This adds a few convenience lemmas for C⋆-rings regarding criteria for being equal, or not equal, to zero.