Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-31 18:58 1fd5195f

View on Github →

chore(data/equiv/mul_add): review (#2874)

  • make mul_aut and add_aut reducible to get coe_fn
  • add some coe_* lemmas

Estimated changes

added theorem add_aut.coe_mul
added theorem add_aut.coe_one
added theorem equiv.coe_inv
added theorem equiv.coe_mul_left
added theorem equiv.coe_mul_right
added theorem equiv.inv_symm
added theorem equiv.mul_left_symm
added theorem equiv.mul_right_symm
added theorem mul_aut.coe_mul
added theorem mul_aut.coe_one