English
The linear independence of a basis follows from its representation: if x,y have same coefficients, then they are equal.
Русский
Линейная независимость базиса вытекает из представления: если коэффициенты совпадают, то векторы равны.
LaTeX
$$$\text{LinearIndependent}(R, b) \Leftrightarrow \forall x,y, x\neq y\Rightarrow (\text{coefficients})\neq (\text{coefficients})$.$$
Lean4
/-- A linear independent family of vectors spanning the whole module is a basis. -/
protected noncomputable def mk : Basis ι R M :=
.ofRepr
{
hli.repr.comp
(LinearMap.id.codRestrict _ fun _ =>
hsp Submodule.mem_top) with
invFun := Finsupp.linearCombination _ v
left_inv := fun x => hli.linearCombination_repr ⟨x, _⟩
right_inv := fun _ => hli.repr_eq rfl }
