mathlib

0b86bb8d - feat(measure_theory/group/arithmetic): actions by int and nat are measurable (#12464)

feat(measure_theory/group/arithmetic): actions by int and nat are measurable (#12464) The `has_measurable_smul₂` proofs are essentially copied from the analogous proofs for `has_measurable_pow`, after golfing them.