mathlib3
8d8b64e5 - feat(data/equiv/mul_add_aut): adding conjugation in an additive group (#6774)

Commit
4 years ago
feat(data/equiv/mul_add_aut): adding conjugation in an additive group (#6774) assuming `[add_group G]` this defines `G ->+ additive (add_aut G)` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
ashwiniyengar
Parents
Loading