unop — Mathlib

English

The unop operation is the inverse of op on AlgHom between opposites.

Русский

Операция unop является обратной к op на AlgHom между противоположностями.

LaTeX

$$unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ A →ₐ[R] B$$

Lean4

/-- The 'unopposite' of an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. Inverse to `RingHom.op`. -/
abbrev unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) :=
  AlgHom.op.symm

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