Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information