mathlib
8792402d - feat(analysis/complex): define `complex.unit_disc` (#17119)

Commit

3 years ago

feat(analysis/complex): define `complex.unit_disc` (#17119)

Author

urkud

urkud

Parents

Loading