snd_comp_toProd — Mathlib

English

Let M and N be monoids. For every x in M ∗ N, the second coordinate of its image under the toProd map equals the second projection of x.

Русский

Пусть M и N — моноиды. Для каждого x в M ∗ N второй компонент образа под toProd совпадает с второй проекцией x.

LaTeX

$$$ \forall x \in M \ast N,\; \operatorname{snd}(\operatorname{toProd}(x)) = \operatorname{snd}(x). $$$

Lean4

@[to_additive (attr := simp) snd_comp_toProd]
theorem snd_comp_toProd : (MonoidHom.snd M N).comp toProd = snd := by rw [← fst_prod_snd, MonoidHom.snd_comp_prod]

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