lift_comp_inr — Mathlib

English

Let M,N,P be monoids and f:M →* P, g:N →* P be monoid homomorphisms. The composition of lift f g with inr equals g; i.e., (lift f g) ∘ inr = g.

Русский

Пусть M, N, P — моноиды и f:M →* P, g:N →* P — моноид-гомоморфизмы. Композиция lift f g с inr даёт g; то есть (lift f g) ∘ inr = g.

LaTeX

$$$\\\\forall f:M \\\\to^* P\\\\, \\\\forall g:N \\\\to^* P\\\\, ((lift f g) \\\\circ inr) = g.$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_comp_inr (f : M →* P) (g : N →* P) : (lift f g).comp inr = g :=
  rfl

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