Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-17 12:21 86b09715

View on Github →

feat(algebra/group_with_zero): Bundled monoid_with_zero_hom (#4995) This adds, without notation, monoid_with_zero_hom as a variant of A →* B that also satisfies f 0 = 0. As part of this, this change:

  • Splits up group_with_zero into multiple files, so that the definitions can be used in the bundled homs before any of the lemmas start pulling in dependencies
  • Adds monoid_with_zero_hom as a base class of ring_hom
  • Changes some monoid_hom objects into monoid_with_zero_hom objects.
  • Moves some lemmas about valuation into monoid_hom, since they apply more generally
  • Add automatic coercions between monoid_with_zero_hom and monoid_hom

Estimated changes

modified theorem ring_hom.map_div
modified theorem ring_hom.map_eq_zero
modified theorem ring_hom.map_inv
modified theorem ring_hom.map_ne_zero
added theorem inv_zero
added theorem mul_inv_cancel
added theorem mul_left_cancel'
added theorem mul_right_cancel'
added theorem mul_zero
added theorem zero_mul
modified theorem valuation.coe_coe
modified theorem
modified def
deleted theorem valuation.map_neg_one
modified theorem valuation.unit_map_eq
modified structure valuation