mathlib3

f721cdca - feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming from an alternating map (#17583)

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.