coe_id — Mathlib

English

The identity morphism in GrpCat, viewed as a function, is the identity function on the underlying set.

Русский

Идентичный морфизм в GrpCat, рассматриваемый как отображение, является тождественной функцией на базовом множестве.

LaTeX

$$$(\mathbb{1} X : X \to X) = \mathrm{id}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_id {X : GrpCat} : (𝟙 X : X → X) = id :=
  rfl

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