Commit 2026-03-04 14:59 2a8445b5

feat(MeasureTheory): Strong measurability is preserved under division in a group with zero (#34427) I proved that if f,g are two strongly measurable functions taking values in a group with zero, then f/g is still strongly measurable. As mentioned over here #Is there code for X? > StronglyMeaurable.div₀, I probably should also change the name of MeasureTheory.StronglyMeasurable.div into StronglyMeasurable.div' according to the docstring of ContinuousDiv. If I do this, then @to_additive will generate a theorem named StronglyMeasurable.sub', which is a bit weird, so I am unsure whether I should change these names.