Commit 2020-11-11 22:13 67309a44
View on Github →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.