mathlib3

726d2fe4 - feat(measure_theory/constructions/prod): marginal measures (#18915)

feat(measure_theory/constructions/prod): marginal measures (#18915) For `ρ : measure (α × β)`, define `ρ.fst : measure α := ρ.map prod.fst`, and define `ρ.snd` similarly.