ofHom_id — Mathlib

English

The ofHom of an identity BialgHom is the identity morphism in the corresponding CommBialgCat object.

Русский

ofHom тождественного биалгебрового гомоморфизма равен тождественному морфизму соответствующего объекта CommBialgCat.

LaTeX

$$$\mathrm{ofHom}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{CommBialgCat.of}(R,X)}$$$

Lean4

@[simp]
theorem ofHom_id : ofHom (.id R X) = 𝟙 (of R X) :=
  rfl

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