# Commit 2022-12-13 06:33 f721cdca

View on Github →feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming from an alternating map (#17583)
To an `n`

-alternating form `ω`

on an `n`

-dimensional space, we associate a Lebesgue measure `ω.measure`

. We show that it satisfies `ω.measure (parallelepiped v) = |ω v|`

when `v`

is a family of `n`

vectors, where `parallelepiped v`

is the parallelepiped spanned by these vectors.
In the special case of inner product spaces, this gives a canonical measure when one takes for the alternating form the canonical one associated to some orientation. Therefore, we register a `measure_space`

instance on finite-dimensional inner product spaces. As the real line is a special case of inner product space, we need to redefine the Lebesgue measure there to avoid having two competing `measure_space`

instances.