Theorems · Definition · category theory

MulEquiv.toSemigrpIso

{X Y : Type u} → [inst : Semigroup X] → [inst_1 : Semigroup Y] → X ≃* Y → (Semigrp.of X ≅ Semigrp.of Y)

Build an isomorphism in the category Semigroup from a MulEquiv between Semigroups.

Defined in

Mathlib.Algebra.Category.Semigrp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemigroupSemigroup