mathlib3
0837fc30 - feat(measure_theory/pi): finite products of measures (#5414)

Commit

4 years ago

feat(measure_theory/pi): finite products of measures (#5414) See module doc of `measure_theory/pi.lean`

Author

fpvandoorn

Parents