English
The domain congruence linear equivalence commutes with the addition in Finsupps.
Русский
Линеарное соответствие доменных конгруаций коммутирует с операцией сложения в Finsupp.
LaTeX
$$$$ (Finsupp.domCongr e).map_add' = \mathrm{?} $$$$
Lean4
/-- An equivalence of domains induces a linear equivalence of finitely supported functions.
This is `Finsupp.domCongr` as a `LinearEquiv`.
See also `LinearMap.funCongrLeft` for the case of arbitrary functions. -/
protected def domLCongr {α₁ α₂ : Type*} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M :=
(Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by
simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul
