Commit 2026-02-16 11:12 2967017d

View on Github →

feat(Algebra/Group/End): use to_additive (#35179) This PR uses to_additive on some lemmas about the instance Group (Perm α). This PR also exposes some technical debt in the form of to_additive being used where it should not. It also swaps the names of AddAut.inv_apply_self and AddAut.apply_inv_self, because they were the wrong way around. This PR revives my old PR #29145

Estimated changes

deleted def Equiv.Perm.MulAut
deleted theorem Equiv.Perm.addLeft_add
deleted theorem Equiv.Perm.addLeft_zero
deleted theorem Equiv.Perm.addRight_add
deleted theorem Equiv.Perm.addRight_zero
deleted theorem Equiv.Perm.inv_addLeft
deleted theorem Equiv.Perm.inv_addRight
modified theorem Equiv.Perm.inv_mulLeft
modified theorem Equiv.Perm.inv_mulRight
modified theorem Equiv.Perm.mulLeft_mul
modified theorem Equiv.Perm.mulLeft_one
modified theorem Equiv.Perm.mulRight_mul
modified theorem Equiv.Perm.mulRight_one
deleted theorem Equiv.Perm.pow_addLeft
deleted theorem Equiv.Perm.pow_addRight
modified theorem Equiv.Perm.pow_mulLeft
modified theorem Equiv.Perm.pow_mulRight
deleted theorem Equiv.Perm.zpow_addLeft
deleted theorem Equiv.Perm.zpow_addRight
modified theorem Equiv.Perm.zpow_mulLeft
modified theorem Equiv.Perm.zpow_mulRight