Theorems · Definition · category theory

AddEquiv.toAddMonCatIso

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

Build an isomorphism in the category AddMonCat from an AddEquiv between AddMonoids.

Defined in

Mathlib.Algebra.Category.MonCat.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoid