mathlib

83965a02 - chore(measure_theory/group/basic): drop measurability assumption