unop — Mathlib

English

The unopposite of a ring hom from Rᵐᵒᵖ to Sᵐᵒᵖ is the inverse of op.

Русский

Обратное отображение кольцевого гомоморфизма Rᵐᵒᵖ → Sᵐᵒᵖ есть обратное к op.

LaTeX

$$$\text{RingHom}(R^{\mathrm{op}}, S^{\mathrm{op}}) \simeq \text{RingHom}(R,S)$$$

Lean4

/-- The 'unopposite' of a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. Inverse to `RingHom.op`. -/
@[simp]
def unop {R S} [NonAssocSemiring R] [NonAssocSemiring S] : (Rᵐᵒᵖ →+* Sᵐᵒᵖ) ≃ (R →+* S) :=
  RingHom.op.symm

Похожие утверждения