mathlib3
1e3447b8 - chore(data/equiv/mul_add): Split out the group structure on automorphisms (#5281)

Commit
5 years ago
chore(data/equiv/mul_add): Split out the group structure on automorphisms (#5281) This prevents `group_theory.perm.basic` being imported into lots of files that don't care about permutations. The argument here is that `add_aut` is to `add_equiv` as `perm` is to `equiv`: `perm` gets its group structure in a separate file to where `equiv` is defined, so `add_aut`, `mul_aut`, and `ring_aut` should too. This adds back imports of `group_theory.perm.basic` to downstream files that inherited them through `data.equiv.mul_add`.
Author
Parents
Loading