mathlib
a2b00f3c - feat(algebra/opposites): functoriality of the opposite monoid (#8254)

Commit

4 years ago

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

Author

dwarn

Parents

6fa678fb

mathlib a2b00f3c - feat(algebra/opposites): functoriality of the opposite monoid (#8254)

mathlib
a2b00f3c - feat(algebra/opposites): functoriality of the opposite monoid (#8254)