injective — Mathlib

English

If v is linearly independent, then v as a function is injective on ι.

Русский

Если v линейно независим, то как функция v : ι → M она инъективна.

LaTeX

$$$[\\text{Nontrivial }R]\\;\\operatorname{LinearIndependent}(R,v) \\Rightarrow \\operatorname{Injective}v$$$

Lean4

theorem injective [Nontrivial R] (hv : LinearIndependent R v) : Injective v := by
  simpa [comp_def] using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)

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