English
A ring isomorphism f: α ≃+* β induces a ring isomorphism αᵐᵒᵖ ≃+* βᵐᵒᵖ, mapping aᵐᵒᵖ to f(a)ᵐᵒᵖ and vice versa for the inverse.
Русский
Кольцевой изоморфизм f: α ≃+* β порождает изоморфизм αᵐᵒᵖ ≃+* βᵐᵒᵖ, переводящий aᵐᵒᵖ в f(a)ᵐᵒᵖ и наоборот для обратного.
LaTeX
$$$\\operatorname{op}(f) : (\\alpha^{op} \\simeq_+^* \\beta^{op})$$$
Lean4
/-- A ring iso `α ≃+* β` can equivalently be viewed as a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`. -/
@[simps! symm_apply_apply symm_apply_symm_apply apply_apply apply_symm_apply]
protected def op {α β} [Add α] [Mul α] [Add β] [Mul β] : α ≃+* β ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ)
where
toFun f := { AddEquiv.mulOp f.toAddEquiv, MulEquiv.op f.toMulEquiv with }
invFun f := { AddEquiv.mulOp.symm f.toAddEquiv, MulEquiv.op.symm f.toMulEquiv with }
