Commit 2019-03-22 00:28 989efaba

View on Github →

feat(data/equiv/algebra): add add_equiv and mul_equiv (#789)

  • feat(data/equiv/algebra): add monoid_equiv and group_equiv
  • refactor; now using mul_equiv; adding add_equiv
  • tidy
  • namechange broke my code; now fixed
  • next effort
  • switching is_mul_hom back to explicit args
  • removing more implicits
  • typo
  • switching back to implicits (to fix mathlib breakage)
  • Making is_mul_hom and is_add_hom classes
  • adding more to_additive

Estimated changes

added theorem is_mul_hom.comp'
added theorem is_mul_hom.comp
added theorem is_mul_hom.id
added theorem units.map_comp'
added theorem units.map_comp
added theorem units.map_id
added def add_equiv.refl
added def add_equiv.symm
added def add_equiv.trans
added structure add_equiv
added theorem mul_equiv.one
added def mul_equiv.refl
added def mul_equiv.symm
added def mul_equiv.trans
added structure mul_equiv
added def units.map_equiv