Theorems · Theorem · linear algebra

iSupIndep_iff_linearIndependent_of_ne_zero

∀ {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] [IsDomain R]
  [Module.IsTorsionFree R N] {ι : Type u_7} {v : ι → N},
  (∀ (i : ι), v i ≠ 0) → ((iSupIndep fun x => R ∙ v x) ↔ LinearIndependent R v)

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleIsDomainModule.IsTorsionFree