k : Type u_4
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_3
b : Basis ι k M
r : R
i : ι
⊢ LinearEquiv.invFun (basisAux R b) (Finsupp.single i r) = r ⊗ₜ[k] ↑(LinearEquiv.symm b.repr) (Finsupp.single i 1)
k : Type u_4
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_3
b : Basis ι k M
r : R
i : ι
⊢ ↑(LinearEquiv.symm (basis R b).repr) (Finsupp.single i r) = r ⊗ₜ[k] ↑(LinearEquiv.symm b.repr) (Finsupp.single i 1)
rw [basis, LinearEquiv.coe_symm_mk]
no goals
k : Type u_4
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_3
b : Basis ι k M
r : R
i : ι
⊢ LinearEquiv.invFun (basisAux R b) (Finsupp.single i r) = r ⊗ₜ[k] ↑(LinearEquiv.symm b.repr) (Finsupp.single i 1)
simp [Equiv.uniqueProd_symm_apply, basisAux]