mathlib3
beee9ecb - feat(data/complex): real part of sum (#14177)

Commit

3 years ago

feat(data/complex): real part of sum (#14177) Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>

Author

b-mehta

Parents