Ring antihomomorphisms, isomorphisms, antiisomorphisms and involutions

This file defines ring antihomomorphisms, antiisomorphism and involutions and proves basic properties of them.

Notations

All types defined in this file are given a coercion to the underlying function.

References

• https://en.wikipedia.org/wiki/Antihomomorphism
• https://en.wikipedia.org/wiki/Involution_(mathematics)#Ring_theory

Tags

Ring isomorphism, automorphism, antihomomorphism, antiisomorphism, antiautomorphism, involution