More to_additive

Stream: general

[Yury G. Kudryashov]

I'm going to add additive versions of docs#is_central_scalar and docs#smul_comm_class. My main motivation is to be able to state theorems like docs#measure_theory.is_fundamental_domain.is_mul_left_invariant_map for two commuting multiplicative/additive actions, then apply it to prove the original result.

[Yury G. Kudryashov]

If there are any objections, then please tell me.

[Eric Wieser]

We already have docs#vadd_comm_class, right?

[Eric Wieser]

I guess you meant docs#is_central_scalar and docs#is_scalar_tower?

[Yury G. Kudryashov]

Indeed, I just miss @[to_additive] tags on some lemmas about mul_opposite and smul_comm_class. Thanks!