opMulEquiv_toEquiv — Mathlib

English

The underlying equivalence of the multiplicative opposite construction equals the standard opposite equivalence.

Русский

Пусть на типе A задано умножение; соответствие opMulEquiv как обычная эквивалентность между A и Aᵐᵒᵖ совпадает с opEquiv.

LaTeX

$$$\bigl(\text{opMulEquiv} : \alpha \simeq^* \alpha^{\mathrm{op}}\bigr) \vert_\alpha = \text{opEquiv}$$$

Lean4

@[simp]
theorem opMulEquiv_toEquiv [Mul α] : ((opMulEquiv : α ≃* αᵃᵒᵖ) : α ≃ αᵃᵒᵖ) = opEquiv :=
  rfl

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