mathlib

0e4760b3 - refactor(measure_theory): add typeclasses for measurability of operations (#6832)

refactor(measure_theory): add typeclasses for measurability of operations (#6832) With these typeclasses and lemmas we can use, e.g., `measurable.mul` for any type with measurable `uncurry (*)`, not only those with `has_continuous_mul`. New typeclasses: * `has_measurable_add`, `has_measurable_add₂`: measurable left/right addition and measurable `uncurry (+)`; * `has_measurable_mul`, `has_measurable_mul₂`: measurable left/right multiplication and measurable `uncurry (*)`; * `has_measurable_pow`: measurable `uncurry (^)` * `has_measurable_sub`, `has_measurable_sub₂`: measurable left/right subtraction and measurable `λ (a, b), a - b` * `has_measurable_div`, `has_measurable_div₂` : measurability of division as a function of numerator/denominator and measurability of `λ (a, b), a / b`; * `has_measurable_neg`, `has_measurable_inv`: measurable negation/inverse; * `has_measurable_const_smul`, `has_measurable_smul`: measurable `λ x, c • x` and measurable `λ (c, x), c • x`