English
For an equivalence e: α ≃ β, there is a natural additive equivalence between finitely supported functions on α and β, given by composing with e and e^{-1} on the domain.
Русский
Для эквиваленты e: α ≃ β существует естественная аддитивная эквивалентность между функциями с конечной опорой на α и на β, получаемая путем композиции с e и e^{-1} по области определения.
LaTeX
$$$\\mathrm{domCongr}\\; e : (\\alpha →₀ M) ≃+ (\\beta →₀ M)$$$
Lean4
/-- Given `AddCommMonoid M` and `e : α ≃ β`, `domCongr e` is the corresponding `Equiv` between
`α →₀ M` and `β →₀ M`.
This is `Finsupp.equivCongrLeft` as an `AddEquiv`. -/
@[simps apply]
protected def domCongr [AddCommMonoid M] (e : α ≃ β) : (α →₀ M) ≃+ (β →₀ M)
where
toFun := equivMapDomain e
invFun := equivMapDomain e.symm
left_inv
v := by
simp_rw [← equivMapDomain_trans, Equiv.self_trans_symm]
exact equivMapDomain_refl _
right_inv := by
intro v
simp_rw [← equivMapDomain_trans, Equiv.symm_trans_self]
exact equivMapDomain_refl _
map_add' a b := by simp only [equivMapDomain_eq_mapDomain, mapDomain_add]
