Theorem MeasureTheory.Measure.sum_of_empty

Modification history

2024-06-16 19:40
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
chore: Golf `Finset.prod_ite_of_true` (#13726) …
Deleted MeasureTheory.Measure.sum_of_emptyView on Github →
2023-05-09 05:50
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
feat: port MeasureTheory.Measure.MeasureSpace (#3324) …
Added MeasureTheory.Measure.sum_of_emptyView on Github →