English
Construct a RingInvo R from a ring homomorphism f: R →+* Rᵐᵒᵖ together with an involution condition ⟦∀ r, (f (f r).unop).unop = r⟧; the resulting object is RingInvo R.
Русский
Построить RingInvo R из кольцеобразного гомоморфа f: R →+* Rᵐᵒᵖ вместе с условием инволюции ∀ r, (f (f r).unop).unop = r; получаемый объект RingInvo R.
LaTeX
$$$\text{mk'}:\ (R\to R^{\mathrm{op}})\to (\forall r, (f(f(r)).unop).unop = r)\to \mathrm{RingInvo}(R).$$$
Lean4
/-- Construct a ring involution from a ring homomorphism. -/
def mk' (f : R →+* Rᵐᵒᵖ) (involution : ∀ r, (f (f r).unop).unop = r) : RingInvo R :=
{ f with
invFun := fun r => (f r.unop).unop
left_inv := fun r => involution r
right_inv := fun _ => MulOpposite.unop_injective <| involution _
involution' := involution }
