English
If g preserves addition (g 0 = 0 and g(x+y) = g x + g y), then mapDomain f and mapRange g commute on v: mapDomain f (mapRange g h0 v) = mapRange g h0 (mapDomain f v).
Русский
Если g сохраняет сложение (g 0 = 0 и g(x+y) = g x + g y), то mapDomain f и mapRange g коммютируют на v: mapDomain f (mapRange g h0 v) = mapRange g h0 (mapDomain f v).
LaTeX
$$$$ mapDomain\ f\ (mapRange\ g\ h0\ v) = mapRange\ g\ h0\ (mapDomain\ f\ v). $$$$
Lean4
/-- When `g` preserves addition, `mapRange` and `mapDomain` commute. -/
theorem mapDomain_mapRange [AddCommMonoid N] (f : α → β) (v : α →₀ M) (g : M → N) (h0 : g 0 = 0)
(hadd : ∀ x y, g (x + y) = g x + g y) : mapDomain f (mapRange g h0 v) = mapRange g h0 (mapDomain f v) :=
let g' : M →+ N :=
{ toFun := g
map_zero' := h0
map_add' := hadd }
DFunLike.congr_fun (mapDomain.addMonoidHom_comp_mapRange f g') v
