mulUnop — Mathlib

English

The inverse correspondence to AddMonoidEnd.toMultiplicative gives an equivalence AddMonoid.End M ≃ Monoid.End (Multiplicative M).

Русский

Обратное соответствие к AddMonoid.End.toMultiplicative образует эквивалентность AddMonoid.End M ≃ Monoid.End (Multiplicative M).

LaTeX

$$$\\mathrm{End}_{AddMonoid}(M) \\simeq \\mathrm{End}_{Monoid}(\\mathrm{Multiplicative} M)$$$

Lean4

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

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