Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.measurable_equiv_real_prod

Modification history

2021-11-21 20:56
src/measure_theory/measure/complex_lebesgue.lean
feat(measure_theory): define volume on `complex` (#10403)
Added complex.measurable_equiv_real_prodView on Github →