feat(group_theory/group_action/sum): Scalar action on a sum of types (#14818)
feat(group_theory/group_action/sum): Scalar action on a sum of types (#14818)

`has_scalar α β → has_scalar α γ → has_scalar α (β ⊕ γ)` and similar.





leanprover-community/mathlib,leanprover-community/mathlib