Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-21 20:56 8ee634b0

View on Github →

feat(measure_theory): define volume on complex (#10403)

Estimated changes

Created src/measure_theory/measure/complex_lebesgue.lean

added def complex.measurable_equiv_pi

added def complex.measurable_equiv_real_prod

added theorem complex.volume_preserving_equiv_pi

added theorem complex.volume_preserving_equiv_real_prod