mathlib3

67309a44 - refactor(group_theory/group_action): Break the file into three pieces (#4936)

refactor(group_theory/group_action): Break the file into three pieces (#4936) I found myself fighting import cycles when trying to define `has_scalar` instances in files that are early in the import tree. By creating a separate `defs` file with minimal dependencies, this ought to become easier. This also adds documentation. None of the proofs or lemma statements have been touched.