linearMap_eq_zero_iff_of_span_eq_top

English

Let V be a submodule with span_R S = V = ⊤; a linear map f: V→N is zero iff it is zero on all elements corresponding to S.

Русский

Если V покрыто span(R,S) и равно ⊤, то нулевость f на V эквивалентна нулевости на каждом s∈S.

LaTeX

$$$(V=\operatorname{span}_R S) \Rightarrow (f=0 \iff \forall s\in S, f(s)=0)$$$

Lean4

theorem linearMap_eq_zero_iff_of_span_eq_top (f : M →ₗ[R] N) {S : Set M} (hM : span R S = ⊤) :
    f = 0 ↔ ∀ (s : S), f s = 0 :=
  linearMap_eq_iff_of_span_eq_top f 0 hM

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