no goals
ι : Type u_3
ι' : Type ?u.68644
R : Type u_1
R₂ : Type ?u.68650
K : Type ?u.68653
M : Type u_2
M' : Type ?u.68659
M'' : Type ?u.68662
V : Type u
V' : Type ?u.68667
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ x : M
⊢ (∀ (i : ι), ↑(coord b i) x = 0) ↔ ↑b.repr x = 0
simp only [b.coord_apply, FunLike.ext_iff, Finsupp.zero_apply]