unop — Mathlib

English

The 'unop' operation, giving an equivalence from opposite rings to ordinary rings, is the inverse of op.

Русский

Операция unop, переходящая от противоположных колец к обычным кольцам, является обратной к op.

LaTeX

$$$\\mathrm{unop} = \\mathrm{op}^{-1}$$$

Lean4

/-- The 'unopposite' of a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`. Inverse to `RingEquiv.op`. -/
@[simp]
protected def unop {α β} [Add α] [Mul α] [Add β] [Mul β] : αᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β) :=
  RingEquiv.op.symm

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