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

Modified src/analysis/complex/basic.lean

added def complex.equiv_real_prod_add_hom

added def complex.equiv_real_prod_add_hom_lm

added def complex.equiv_real_prodₗ

added theorem complex.has_sum_iff

Modified src/topology/algebra/infinite_sum.lean

added theorem has_sum.prod_mk