snd_comp_swap — Mathlib

English

Let M and N be monoids. The second projection after swapping equals the first projection before swapping: snd ∘ swap = fst.

Русский

Пусть M и N — моноиды. Вторая проекция после перестановки равна первой до перестановки: snd ∘ swap = fst.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem snd_comp_swap : snd.comp (swap M N) = fst :=
  lift_comp_swap _ _

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