LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent.Defs #
Imported Lean Pool material for
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent.Defs.
theorem
linearIndependent_iff_linearIndepOn_finset
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
: