Theorem MeasureTheory.Measure.pi_map_piCongrLeft

Modification history

2026-04-24 10:37

Mathlib/MeasureTheory/Constructions/Pi.lean

refactor(MeasureTheory): golf `Mathlib/MeasureTheory/Constructions/Pi` (#38353) …

Modified MeasureTheory.Measure.pi_map_piCongrLeft View on Github →

2024-06-13 00:50

Mathlib/MeasureTheory/Constructions/Pi.lean

feat: Add lemmas about finite products of measures (#13311) …

Added MeasureTheory.Measure.pi_map_piCongrLeft View on Github →