Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-05 20:33 0c8fffe9

View on Github →

fix(algebra/group/prod): fixes for #5563 (#5577)

  • rename prod.units to mul_equiv.prod_units;
  • rewrite it with better definitional equalities;
  • now @[to_additive] works: fixes #5566;
  • make M and N implicit in mul_equiv.prod_comm

Estimated changes

modified theorem mul_equiv.coe_prod_comm
deleted def prod.units
added theorem units.inv_mk
added theorem units.mk_coe
modified theorem ring_equiv.coe_prod_comm