mulUnop — Mathlib

English

The inverse correspondence to AddHom.mulOp gives an equivalence between AddHom M^op N^op and AddHom M N, via the unop operation.

Русский

Обратное соответствие к AddHom.mulOp задаёт эквивалентность между AddHom M^op N^op и AddHom M N через операцию разоплощения.

LaTeX

$$$\\operatorname{AddHom}(M^{op},N^{op}) \\simeq \\operatorname{AddHom}(M,N)$$$

Lean4

/-- The 'unopposite' of an additive semigroup hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
`AddHom.mul_op`. -/
@[simp]
def mulUnop {α β} [Add α] [Add β] : AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β :=
  AddHom.mulOp.symm

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