Commit 2020-11-11 22:13 67309a44

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.