no goals
ι : Type u_1
ι' : Type ?u.32722
R : Type u_2
R₂ : Type ?u.32728
K : Type ?u.32731
M : Type u_3
M' : Type ?u.32737
M'' : Type ?u.32740
V : Type u
V' : Type ?u.32745
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 : M
j : ι
inst✝ : Decidable (i = j)
⊢ ↑(↑b.repr (↑b i)) j = if i = j then 1 else 0
rw [repr_self, Finsupp.single_apply]