no goals
ι : Type u_1
ι' : Type ?u.670971
R : Type u_2
R₂ : Type ?u.670977
K : Type ?u.670980
M : Type u_3
M' : Type ?u.670986
M'' : Type ?u.670989
V : Type u
V' : Type ?u.670994
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Fintype ι
b : Basis ι R M
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(equivFun b) (↑b i) j = if i = j then 1 else 0
rw [b.equivFun_apply, b.repr_self_apply]