Theorems · Definition · category theory

AddSemigrp.ofHom

{X Y : Type u} → [inst : AddSemigroup X] → [inst_1 : AddSemigroup Y] → (X →ₙ+ Y) → (AddSemigrp.of X ⟶ AddSemigrp.of Y)

Typecheck an AddHom as a morphism in AddSemigrp.

Defined in

Mathlib.Algebra.Category.Semigrp.Basic

Cited by

8 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

AddSemigroupAddSemigroup