Def MeasureTheory.IsSetRing.addContent_of_union

Modification history

2026-01-26 08:43
Mathlib/MeasureTheory/Measure/AddContent.lean
feat: let `AddContent` take values in a general monoid (#34434) …
Modified MeasureTheory.IsSetRing.addContent_of_unionView on Github →
2025-01-24 07:58
Mathlib/MeasureTheory/Measure/AddContent.lean
feat(MeasureTheory): additive contents on rings of sets (#20977) …
Added MeasureTheory.IsSetRing.addContent_of_unionView on Github →