mathlib

4e17e081 - feat(data/complex/basic): re-im set product (#11770)

feat(data/complex/basic): re-im set product (#11770) `set.re_im_prod s t` (notation: `s ×ℂ t`) is the product of a set on the real axis and a set on the imaginary axis of the complex plane.