arithmetic): add `has_measurable_smul.op` and `has_measurable_smul₂.op` (#12196)

Commit

3 years ago

feat(measure_theory/group/arithmetic): add `has_measurable_smul.op` and `has_measurable_smul₂.op` (#12196) This matches the naming of `has_continuous_smul.op`.

Author

eric-wieser

Parents

79c5de9a

mathlib 8b09b0ec - feat(measure_theory/group/arithmetic): add `has_measurable_smul.op` and `has_measurable_smul₂.op` (#12196)

mathlib
8b09b0ec - feat(measure_theory/group/arithmetic): add `has_measurable_smul.op` and `has_measurable_smul₂.op` (#12196)