Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 13:06 beee9ecb

View on Github →

feat(data/complex): real part of sum (#14177)

Estimated changes

Modified src/data/complex/basic.lean

added theorem complex.im_sum

modified theorem complex.of_real_prod

modified theorem complex.of_real_sum

added theorem complex.re_sum