Mathlib v3 is deprecated. Go to Mathlib v4

Def set.re_prod_im

Modification history

2022-02-09 08:51
src/data/complex/basic.lean
feat(data/complex/basic): re-im set product (#11770) …
Added set.re_prod_imView on Github →