coe_of — Mathlib

English

An extensional lemma for CommGrpCat: equality of morphisms follows from equality of their underlying Hom components.

Русский

Лемма экстенсионности для CommGrpCat: равенство морфизмов следует из равенства их базовых компонентов hом.

LaTeX

$$$ \\forall \\; f,g:\\, X \\to Y,\\; f.hom = g.hom \\Rightarrow f = g $$$

Lean4

@[to_additive]
  -- This is not `simp` to avoid rewriting in types of terms.

theorem coe_of (R : Type u) [CommGroup R] : ↑(CommGrpCat.of R) = R :=
  rfl

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