mathlib3
2efabeb7 - feat(group_theory/group_action/defs): `is_central_vadd` (#17446)

Commit
3 years ago
feat(group_theory/group_action/defs): `is_central_vadd` (#17446) Define `is_central_vadd`, the additive version of `is_central_scalar`. Tag a few forgotten declarations with `to_additive`.
Author
Parents
Loading