Commit 2024-11-28 13:58 bbf85a5e

View on Github →

feat(MeasureTheory): add Measure.fst_add, Measure.fst_sum (#19564) and similar lemmas for snd.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Prod.lean

added theorem MeasureTheory.Measure.fst_add

added theorem MeasureTheory.Measure.fst_sum

added theorem MeasureTheory.Measure.snd_add

added theorem MeasureTheory.Measure.snd_sum