Ring involutions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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ᵐᵒᵖ.
A ring involution
The equivalence of rings underlying a ring involution.
ring_invo_class F R S states that
F is a type of ring involutions.
You should extend this class when you extend
Instances of this typeclass
Instances of other typeclasses for
Construct a ring involution from a ring homomorphism.
Helper instance for when there's too many metavariables to apply
The identity function of a
comm_ring is a ring involution.