snd_toProd — Mathlib

English

Let M and N be monoids. Regard swap as exchanging the two factors; then the first projection after swapping equals the second projection before swapping.

Русский

Пусть M и N — моноиды. Переключение (swap) меняет местами факторы; тогда первая проекция после перестановки равна второй проекции до перестановки.

LaTeX

$$$ \mathrm{fst} \circ (\mathrm{swap}\ M\ N) = \mathrm{snd}. $$$

Lean4

@[to_additive (attr := simp) snd_toProd]
theorem snd_toProd (x : M ∗ N) : (toProd x).2 = snd x := by rw [← snd_comp_toProd]; rfl

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