Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-20 08:43 e174f42c

View on Github →

feat(equiv/transfer_instances): other algebraic structures (#3870) Some updates to data.equiv.transfer_instances.

  1. Use @[to_additive]
  2. Add algebraic equivalences between the original and transferred instances.
  3. Transfer modules and algebras.

Estimated changes

deleted theorem equiv.add_def
added def equiv.alg_equiv
added def equiv.mul_equiv
added theorem equiv.mul_equiv_apply
deleted theorem equiv.neg_def
added def equiv.ring_equiv
added theorem equiv.ring_equiv_apply
added theorem equiv.smul_def
deleted theorem equiv.zero_def