Commit 2022-04-19 14:04 8f7e10b8
View on Github →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