Theorems · Theorem · linear algebra

Finsupp.linearIndependent_single_of_ne_zero

∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [IsDomain R]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] {v : ι → M},
  (∀ (i : ι), v i ≠ 0) → LinearIndependent R fun i => fun₀ | i => v i

Defined in

Mathlib.LinearAlgebra.Finsupp.VectorSpace

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupIsDomainModuleModule.IsTorsionFree