Zulip Chat Archive

Stream: general

Topic: linear independent

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 = ⊥

Kenny Lau (May 24 2020 at 19:56):

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

Johan Commelin (May 25 2020 at 04:51):

Sounds good to me!

Last updated: Dec 20 2023 at 11:08 UTC