addMonoidHom_comp_mapRange — Mathlib

English

For all f : α → β and g : M →+ N, the two ways of composing with mapDomain f and mapRange g commute.

Русский

Для любых f : α → β и g : M →+ N операции композиций с mapDomain f и mapRange g commutируют.

LaTeX

$$$$ (\mathrm{mapDomain.} \mathrm{addMonoidHom}\ f)\circ (\mathrm{mapRange.} \mathrm{addMonoidHom}\ g) = (\mathrm{mapRange.} \mathrm{addMonoidHom}\ g)\circ (\mathrm{mapDomain.} \mathrm{addMonoidHom}\ f). $$$$

Lean4

theorem addMonoidHom_comp_mapRange [AddCommMonoid N] (f : α → β) (g : M →+ N) :
    (mapDomain.addMonoidHom f).comp (mapRange.addMonoidHom g) =
      (mapRange.addMonoidHom g).comp (mapDomain.addMonoidHom f) :=
  by
  ext
  simp

Похожие утверждения