Commit 2020-12-08 22:41 1e3447b8

View on Github →

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.

Estimated changes

deleted theorem add_aut.apply_inv_self
deleted theorem add_aut.coe_mul
deleted theorem add_aut.coe_one
deleted theorem add_aut.inv_apply_self
deleted theorem add_aut.inv_def
deleted theorem add_aut.mul_apply
deleted theorem add_aut.mul_def
deleted theorem add_aut.one_apply
deleted theorem add_aut.one_def
deleted def add_aut.to_perm
deleted theorem mul_aut.apply_inv_self
deleted theorem mul_aut.coe_mul
deleted theorem mul_aut.coe_one
deleted def mul_aut.conj
deleted theorem mul_aut.conj_apply
deleted theorem mul_aut.conj_inv_apply
deleted theorem mul_aut.conj_symm_apply
deleted theorem mul_aut.inv_apply_self
deleted theorem mul_aut.inv_def
deleted theorem mul_aut.mul_apply
deleted theorem mul_aut.mul_def
deleted theorem mul_aut.one_apply
deleted theorem mul_aut.one_def
deleted def mul_aut.to_perm
deleted def mul_aut
added theorem add_aut.apply_inv_self
added theorem add_aut.coe_mul
added theorem add_aut.coe_one
added theorem add_aut.inv_apply_self
added theorem add_aut.inv_def
added theorem add_aut.mul_apply
added theorem add_aut.mul_def
added theorem add_aut.one_apply
added theorem add_aut.one_def
added def add_aut.to_perm
added theorem mul_aut.apply_inv_self
added theorem mul_aut.coe_mul
added theorem mul_aut.coe_one
added def mul_aut.conj
added theorem mul_aut.conj_apply
added theorem mul_aut.conj_inv_apply
added theorem mul_aut.inv_apply_self
added theorem mul_aut.inv_def
added theorem mul_aut.mul_apply
added theorem mul_aut.mul_def
added theorem mul_aut.one_apply
added theorem mul_aut.one_def
added def mul_aut.to_perm
added def mul_aut