unop — Mathlib

English

The unop is the inverse of op; it provides an equivalence MulEquiv α^op β^op ≃ (MulEquiv α β).

Русский

Разоплощение является обратной операцией к Opposite; образует эквиваленцию MulEquiv α^op β^op ≃ MulEquiv α β.

LaTeX

$$$\\mathrm{MulEquiv}(α^{op},β^{op}) \\simeq \\mathrm{MulEquiv}(α,β)$$$

Lean4

/-- The 'unopposite' of an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. Inverse to `MulEquiv.op`. -/
@[to_additive (attr := simp) /-- The 'unopposite' of an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`. Inverse to `AddEquiv.op`. -/
    ]
def unop {α β} [Mul α] [Mul β] : αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β) :=
  MulEquiv.op.symm

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