mathlib

8f7e10b8 - refactor(group_theory/group_action/big_operators): extract to a new file (#13340)

refactor(group_theory/group_action/big_operators): extract to a new file (#13340) `basic` is a misleading name, as `group_action.basic` imports a lot of things. For now I'm not renaming it, but I've adding a skeletal docstring. Splitting out the big operator lemmas allows access to big operators before modules and quotients. This also performs a drive-by generalization of the typeclasses on `smul_cancel_of_non_zero_divisor`. Authorship is from #1910