Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.equiv_real_prod_add_hom_lm

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_add_hom_lmView 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_add_hom_lmView on Github →