opposite): `{ring,monoid}_hom.from_opposite` (#10723)

Commit

4 years ago

feat(algebra/{group,ring}/opposite): `{ring,monoid}_hom.from_opposite` (#10723) We already have the `to_opposite` versions.

Author

eric-wieser

Parents