ofHom_apply — Mathlib

English

For X,Y commutative groups and f: X →* Y, for any x ∈ X, the underlying map of (ofHom f) sends x to f(x).

Русский

Пусть X,Y — коммутационные группы и f: X →* Y. Для любого x ∈ X подлежащая функция у (ofHom f) действует так, что (ofHom f)(x) = f(x).

LaTeX

$$$$ \forall X,Y\,[\mathrm{CommGroup}(X)], [\mathrm{CommGroup}(Y)],\ (f : X \to_* Y),\ (\mathrm{ofHom}(f))(x) = f(x). $$$$

Lean4

@[to_additive]
theorem ofHom_apply {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) : (ofHom f) x = f x :=
  rfl

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