TODO

Rename mapDomain.linearEquiv!

@[simp]

theorem Finsupp.toLinearMap_mapDomainLinearEquiv {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_9} (f : α ≃ α') : ↑(mapDomain.linearEquiv M R f) = lmapDomain M R ⇑f

Alias of Finsupp.mapDomain.toLinearMap_linearEquiv.

@[simp]

theorem Finsupp.coe_mapDomainLinearEquiv {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : α ≃ β) : ⇑(mapDomain.linearEquiv M R e) = equivMapDomain e