Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.of_real_prod

Modification history

2022-05-17 13:06
src/data/complex/basic.lean
feat(data/complex): real part of sum (#14177)
Modified complex.of_real_prodView on Github →
2020-10-05 07:39
src/data/complex/basic.lean
feat(data/complex): norm_cast lemmas (#4405) …
Added complex.of_real_prodView on Github →