Commit 2022-12-13 06:33 f721cdca

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.