rw [linearIndependent_iff]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
N✝ : Submodule R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
N✝ : Submodule R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ ∀ (l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R),
    (Finsupp.total (↑(Set.range ⇑B.snd.f)ᶜ) (M ⧸ N) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)) l = 0 → l = 0