Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.mem_re_prod_im

Modification history

2022-04-11 11:52
src/data/complex/basic.lean
feat(analysis/complex/re_im_topology): add `metric.bounded.re_prod_im` (#13324) …
Added complex.mem_re_prod_imView on Github →