mathlib3
6ed508e2
- chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped`
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped` These are bundled versions of the lemmas about `parallelepiped`.
References
#19013 - feat(measure_theory/measure/haar_lebesgue): the volume measures on `euclidean_space ℝ ι` and `ι → ℝ` agree
Author
eric-wieser
Parents
358d353a
Loading