mathlib3
feat(measure_theory/measure/haar_lebesgue): the volume measures on `euclidean_space ℝ ι` and `ι → ℝ` agree
#19013
Open
Open
feat(measure_theory/measure/haar_lebesgue): the volume measures on `euclidean_space ℝ ι` and `ι → ℝ` agree #19013
eric-wieser
wants to merge
21 commits into
master
from
eric-wieser/euclidean-measurable-2
feat(measure_theory/measure/haar_of_basis): put the canonical measure…
b9e87120
add lemma
b59d0598
wip
006db9c2
wip
bf341beb
feat(topology/sets/compacts): add `positive_compacts.map`
358d353a
chore(measure_theory/measure/haar_of_basis): lemmas about `basis.para…
6ed508e2
Merge remote-tracking branch 'origin/master' into eric-wieser/trivial…
f8ab07ba
Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…
f5bb3b53
Merge remote-tracking branch 'origin/eric-wieser/trivial-basis.parall…
0680ec16
fix bad merge
954e92be
wip
72951777
Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…
e47004c6
reduce diff
cb2bc145
wip
0842c48f
whoops, sloppy types
eb5644a9
remove bad lemma
d1eba19a
wip
afb1e373
revert unrelated tweaks
bf36504a
Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…
2d456635
wip
22e7f9d9
new lemma
32e36cf7
Reviewers
No reviews
Assignees
No one assigned
Labels
WIP
t-measure-probability
modifies-synchronized-file
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub