English
Let R be a semiring, M an R-module, and v: ι → M a family of vectors. The family (v_i)_{i∈ι} is linearly independent over R if the only finite linear relation ∑_{i∈F} a_i v_i = 0 with a_i ∈ R and F ⊆ ι finite is the trivial one a_i = 0 for all i ∈ F.
Русский
Пусть R — полупольр, M — модуль над R, и v : ι → M. Семейство (v_i)_{i∈ι} линейно независимо над R тогда и только тогда, когда любая конечная линейная зависимость ∑_{i∈F} a_i v_i = 0 с a_i ∈ R и F ⊆ ι конечна, влечёт a_i = 0 для всех i ∈ F.
LaTeX
$$$\\operatorname{LinearIndependent}(R,v) \\iff \\operatorname{Injective}\\left(Finsupp.linearCombination\\;R\\;v\\right)$$$
Lean4
/-- `LinearIndependent R v` states the family of vectors `v` is linearly independent over `R`. -/
def LinearIndependent : Prop :=
Injective (Finsupp.linearCombination R v)
