Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-13 12:37 f0348994

View on Github →

feat(data/equiv/mul_add): conj as a mul_aut (#3367)

Estimated changes

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 mul_aut.conj
added theorem mul_aut.conj_apply
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