map_comp_inr — Mathlib

English

Let f: M →* M' and g: N →* N' be monoid homomorphisms. Then the coproduct map (map f g) composed with the right-injection inr equals the right-injection composed with g: (map f g) ∘ inr = inr ∘ g.

Русский

Пусть f: M →* M' и g: N →* N' — гомоморфизмы моноидов. Тогда отображение копрода, действующее как (map f g), при композиции с правой инъекцией inr эквивалентно инъекции, полученной через g: (map f g) ∘ inr = inr ∘ g.

LaTeX

$$$ (\operatorname{map}(f,g)) \circ \mathrm{inr} = \mathrm{inr} \circ g $$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp_inr (f : M →* M') (g : N →* N') : (map f g).comp inr = inr.comp g :=
  rfl

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