chore(analysis/normed_space/star/complex): delete file (#16871)

We now have two versions of this. I am keeping the other one instead of this because: (a) it lives in the right place, (b) it has associated notation, (c) it has slightly more API, and (d) it has already been used somewhere.
leanprover-community · Oct 10, 2022 · 8434f76 · 8434f76
1 parent 91db833
commit 8434f76
Showing 1 changed file with 0 additions and 59 deletions.
diff --git a/src/analysis/normed_space/star/complex.lean b/src/analysis/normed_space/star/complex.lean