map_id — Mathlib

English

The map corresponding to the identity function is the identity map on FreeAbelianGroup α.

Русский

Отображение, соответствующее тождественной функции, равно тождественному отображению на FreeAbelianGroup α.

LaTeX

$$$ \forall {\alpha} \; \operatorname{map} (\mathrm{id}) = \operatorname{id}_{\operatorname{FreeAbelianGroup}(\alpha)} $$$

Lean4

theorem map_id : map id = AddMonoidHom.id (FreeAbelianGroup α) :=
  Eq.symm <| lift_ext _ _ fun _ ↦ lift_unique of (AddMonoidHom.id _) fun _ ↦ AddMonoidHom.id_apply _ _

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