Theorems · Definition · category theory

MulEquiv.toMonCatIso

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

Build an isomorphism in the category MonCat from a MulEquiv between Monoids.

Defined in

Mathlib.Algebra.Category.MonCat.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMonoid