Zulip Chat Archive

Stream: general

Topic: linear independent


view this post on Zulip Kenny Lau (May 24 2020 at 19:56):

https://github.com/leanprover-community/mathlib/blob/8d352b200937598eba3aa303b5acc558713e645a/src/linear_algebra/basis.lean#L78-L79

/-- Linearly independent family of vectors -/
def linear_independent : Prop := (finsupp.total ι M R v).ker = 

view this post on Zulip Kenny Lau (May 24 2020 at 19:56):

should we call this linear**ly**_independent?

view this post on Zulip Johan Commelin (May 25 2020 at 04:51):

Sounds good to me!


Last updated: May 12 2021 at 23:13 UTC