Commit 2021-07-12 17:16 a2b00f3c

View on Github →

feat(algebra/opposites): functoriality of the opposite monoid (#8254) A hom α →* β can equivalently be viewed as a hom αᵒᵖ →* βᵒᵖ. Split off from #7395

Estimated changes

Modified src/algebra/opposites.lean

added def add_monoid_hom.op

added def add_monoid_hom.unop

added def monoid_hom.op

added def monoid_hom.unop

added def ring_hom.op

added def ring_hom.unop