Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-29 13:12 8d8b64e5

View on Github →

feat(data/equiv/mul_add_aut): adding conjugation in an additive group (#6774) assuming [add_group G] this defines G ->+ additive (add_aut G)

Estimated changes

added def add_aut.conj
added theorem add_aut.conj_apply
added theorem add_aut.conj_inv_apply
modified theorem mul_aut.conj_inv_apply