one_apply — Mathlib

English

Let G and H be groups. The underlying function of the identity morphism (1 : G ⟶ H) sends every element g ∈ G to the identity element 1 in H.

Русский

Пусть G и H — группы. Линейный/идентичный морфизм (1 : G ⟶ H) как функция от G к H отправляет каждый элемент g ∈ G в единицу 1 в H.

LaTeX

$$$ ((1 : G \\to H)) (g) = 1 \\quad \\text{for all } g \\in G $$$

Lean4

@[to_additive (attr := simp)]
theorem one_apply (G H : GrpCat) (g : G) : ((1 : G ⟶ H) : G → H) g = 1 :=
  rfl

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