mkIso' — Mathlib

English

Mon Homs are extensional: two monoid morphisms are equal if their underlying homs are equal.

Русский

Гомоморфизмы Mon экстенсиональны: равны, если их подлежащие гомоморфизмы равны.

LaTeX

$$$\\forall f,g:\\,M\\to N,\\; f.hom=g.hom\\Rightarrow f=g$$$

Lean4

/-- Construct an isomorphism of monoid objects by giving a monoid isomorphism between the underlying
objects. -/
@[simps]
def mkIso' {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] : mk M ≅ mk N
    where
  hom := Hom.mk e.hom
  inv := Hom.mk e.inv

Похожие утверждения