Topic: More to_additive
Yury G. Kudryashov (Feb 14 2022 at 01:20):
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 (Feb 14 2022 at 02:29):
If there are any objections, then please tell me.
Eric Wieser (Feb 14 2022 at 08:20):
We already have docs#vadd_comm_class, right?
Eric Wieser (Feb 14 2022 at 08:37):
Yury G. Kudryashov (Feb 14 2022 at 14:57):
Indeed, I just miss
@[to_additive] tags on some lemmas about
Last updated: Aug 03 2023 at 10:10 UTC