mathlib

79887c96 - feat(measure_theory/group/prod): generalize topological groups to measurable groups (#11933)

feat(measure_theory/group/prod): generalize topological groups to measurable groups (#11933) * This fixes the gap in `[Halmos]` that I mentioned in `measure_theory.group.prod` * Thanks to @sgouezel for giving me the proof to fill that gap. * A text proof to fill the gap is [here](https://math.stackexchange.com/a/4387664/463377)