Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-07 07:50 a2a867e8

View on Github →

feat(algebra/ring): bundled semiring homs (#1305)

  • 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

Estimated changes

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