mathlib3

4b884eff - chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped` (#18873)

chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped` (#18873) These are bundled versions of the lemmas about `parallelepiped`. This is working towards the result that the measure on `euclidean_space` and the corresponding pi type agree.