English
For e: α ≃ β and f: β ≃ γ, the composition of domCongr e and domCongr f equals domCongr (e ∘ trans f). In other words, the domain-change is compatible with composition.
Русский
Для e: α ≃ β и f: β ≃ γ композиция domCongr e и domCongr f равна domCongr (e ∘ f). То есть переход по областям совместим с композициями.
LaTeX
$$$(\\mathrm{domCongr} \\; e) \\; \\mathrm{trans} \\; (\\mathrm{domCongr} \\; f) = (\\mathrm{domCongr} \\; (e \\; \\mathrm{trans} \\; f))$$$
Lean4
@[simp]
theorem domCongr_trans [AddCommMonoid M] (e : α ≃ β) (f : β ≃ γ) :
(Finsupp.domCongr e).trans (Finsupp.domCongr f) = (Finsupp.domCongr (e.trans f) : (α →₀ M) ≃+ _) :=
AddEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm
