basic): add a few lemmas about `dist` on `complex` (#14796)

Commit

3 years ago

feat(analysis/complex/basic): add a few lemmas about `dist` on `complex` (#14796)

Author

urkud

Parents