maximal linear independent set?

Stream: Is there code for X?

[Scott Morrison]

What is the colloquial way to talk about a maximal linearly independent family?

[Scott Morrison]

I can't find anything so far, so propose

def maximal_linear_independent {ι : Type*} (v : ι → M) : Prop :=
∀ {κ : Type*} (w : κ → M) (i : linear_independent R v) (h : range v ≤ range w), range v = range w

[Scott Morrison]

But maybe there is a partial order already hiding somewhere that I can appeal to?

[Damiano Testa]

Depending on context, this could mean "span up to finite index", right?

[Scott Morrison]

I'm at the moment setting up the very basics of cardinalities of independent sets / bases / spanning sets over arbitrary rings, so no, "span up to finite index" is far into the future. :-)

[Damiano Testa]

Oh, I see, you were interested in a "Lean colloquial way"! Sorry for misunderstanding!

[Scott Morrison]

Ah, that definition is bad, I need to include that v itself is actually linearly independent. :-)

[Damiano Testa]

w?

[Scott Morrison]

Oops, and there is a typo, the arguments i should say linear_independent R w!

[Kevin Buzzard]

If R is the zero ring then one has to decide what the definition means

[Scott Morrison]

Oh dear. :-) I will paste [nontrivial R] anywhere there are signs of trouble. :-)