Commit 2026-04-24 10:37 b5cacbcf

View on Github →

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

  • refactors MeasureTheory/Constructions/Pi by moving pi_map_piCongrLeft next to measurePreserving_piCongrLeft and deriving it directly from .map_eq Extracted from #38104 Open in Gitpod

Estimated changes