smul_left_injective — Mathlib

English

For any i, if v is LI, then the map r ↦ r · v_i is injective on R.

Русский

Для каждого i, если v линейно независимо, то отображение r ↦ r · v_i сопоставимо инъективно на R.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\Rightarrow \\forall i,\\; \\operatorname{Injective}\\big(\\lambda r:\\,R \\mapsto r\\,\\cdot v_i\\big)$$$

Lean4

theorem smul_left_injective (hv : LinearIndependent R v) (i : ι) : Injective fun r : R ↦ r • v i := by
  convert hv.comp (Finsupp.single_injective i); simp

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