haar_of_basis): put the canonical measure on euclidean space (#18870)

Commit

2 years ago

feat(measure_theory/measure/haar_of_basis): put the canonical measure on euclidean space (#18870)

Author

eric-wieser

Parents