Theorems · Definition · category theory

AddEquiv.toAddSemigrpIso

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

Build an isomorphism in the category AddSemigroup from an AddEquiv between AddSemigroups.

Defined in

Mathlib.Algebra.Category.Semigrp.Basic

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

AddSemigroupAddSemigroup