Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.im_sum

Modification history

2022-05-17 13:06
src/data/complex/basic.lean
feat(data/complex): real part of sum (#14177)
Added complex.im_sumView on Github →