unop — Mathlib

English

The unop operation is inverse to op on AlgEquiv between opposites.

Русский

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

LaTeX

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

Lean4

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

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