Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-10 05:50 8434f767

View on Github →

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.

Estimated changes