Lemmata for module bases

This file just exists until the project can update to mathlib version 4.29 as it has been proven (along with other useful lemmata) there.

theorem Module.Basis.linearIndepOn {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (s : Set ι) : LinearIndepOn R (⇑b) s