Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 04:15 68987280

View on Github →

feat(analysis/complex/basic): a complex-valued function has_sum iff its real part and imaginary part has_sum (#9648)

Estimated changes