Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-19 15:32 ce105fda

View on Github →

chore(algebra/group): rename as_monoid_hom into monoid_hom.of, define ring_hom.of (#1443)

  • chore(algebra/group): rename as_monoid_hom into monoid_hom.of This is similar to Mon.of etc.
  • Fix compile
  • Docs, missing universe
  • Move variables declaration up as suggested by @jcommelin
  • doc-string

Estimated changes

deleted def as_monoid_hom
deleted theorem coe_as_monoid_hom
added theorem monoid_hom.coe_of
added def monoid_hom.of
modified theorem ring_hom.coe_of
modified def ring_hom.of