Ring involutions #
This file defines a ring involution as a structure extending
R ≃+* Rᵒᵖ,
with the additional fact
f.involution : (f (f x).unop).unop = x.
We provide a coercion to a function
R → Rᵒᵖ.
Construct a ring involution from a ring homomorphism.
The identity function of a
comm_ring is a ring involution.