Def complex.equiv_real_prodₗ

Modification history

2023-01-24 03:14
src/analysis/complex/basic.lean
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) …
Deleted complex.equiv_real_prodₗView on Github →
2021-10-20 04:15
src/analysis/complex/basic.lean
feat(analysis/complex/basic): a complex-valued function `has_sum` iff its real part and imaginary part `has_sum` (#9648)
Added complex.equiv_real_prodₗView on Github →