ofHom_apply — Mathlib

English

Let f: M →ₗ[R] N be a linear map and x ∈ M. The morphism corresponding to f sends x to f(x).

Русский

Пусть f: M →ₗ[R] N — линейное отображение и x ∈ M. Соответствующее отображение отправляет x в f(x).

LaTeX

$$$ (\operatorname{ofHom} f)(x) = f(x) $$$

Lean4

theorem ofHom_apply {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (x : M) :
    ofHom f x = f x :=
  rfl

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