Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-26 17:11 cc04ba7e

View on Github →

chore(algebra/ring): change semiring_hom to ring_hom (#1361)

  • added bundled ring homs
  • removed comment
  • Tidy and making docstrings consistent
  • fix spacing
  • fix typo Co-Authored-By: Johan Commelin johan@commelin.net
  • fix typo Co-Authored-By: Johan Commelin johan@commelin.net
  • whoops, actually removing instances
  • change semiring_hom to ring_hom
  • corrected docstring

Estimated changes

added def ring_hom.comp
added theorem ring_hom.ext
added def ring_hom.id
added theorem ring_hom.map_add
added theorem ring_hom.map_mul
added theorem ring_hom.map_neg
added theorem ring_hom.map_one
added theorem ring_hom.map_sub
added theorem ring_hom.map_zero
added def ring_hom.mk'
added structure ring_hom
deleted def semiring_hom.comp
deleted theorem semiring_hom.ext
deleted def semiring_hom.id
deleted theorem semiring_hom.map_add
deleted theorem semiring_hom.map_mul
deleted theorem semiring_hom.map_neg
deleted theorem semiring_hom.map_one
deleted theorem semiring_hom.map_sub
deleted theorem semiring_hom.map_zero
deleted def semiring_hom.mk'
deleted structure semiring_hom