# Lebesgue measure on `ℂ`

#

In this file, we consider the Lebesgue measure on `ℂ`

defined as the push-forward of the volume
on `ℝ²`

under the natural isomorphism and prove that it is equal to the measure `volume`

of `ℂ`

coming from its `InnerProductSpace`

structure over `ℝ`

. For that, we consider the two frequently
used ways to represent `ℝ²`

in `mathlib`

: `ℝ × ℝ`

and `Fin 2 → ℝ`

, define measurable equivalences
(`MeasurableEquiv`

) to both types and prove that both of them are volume preserving (in the sense
of `MeasureTheory.measurePreserving`

).