ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDfinsupp R) = Finsupp.toDfinsupp
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDfinsupp R) = Finsupp.toDfinsupp
simp only [@LinearEquiv.coe_coe]
no goals
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDfinsupp R) = Finsupp.toDfinsupp
rfl