Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-07 20:48 89174191

View on Github →

chore(data/equiv/algebra): use to_additive (#1191)

  • Define add_equiv and add_equiv.* using to_additive
  • Simplify some instances

Estimated changes

deleted def add_equiv.refl
deleted def add_equiv.symm
deleted def add_equiv.trans
deleted theorem mul_equiv.one