Theorems · Definition · category theory

mulEquivIsoSemigrpIso

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

multiplicative equivalences between Semigroups are the same as (isomorphic to) isomorphisms in Semigroup

Defined in

Mathlib.Algebra.Category.Semigrp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemigroupSemigroup