snd — Mathlib

English

The map snd: M × N → N is a monoid homomorphism projecting onto the second coordinate.

Русский

Отображение snd: M × N → N является однородной гомоморфизмом, проекцией на вторую координату.

LaTeX

$$$(\text{snd})( (m,n)\cdot (m',n') ) = (\text{snd}(m,n))\cdot (\text{snd}(m',n'))$$$

Lean4

/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`. -/
@[to_additive /-- Given additive magmas `A`, `B`, the natural projection homomorphism
          from `A × B` to `B` -/
    ]
def snd : M × N →ₙ* N :=
  ⟨Prod.snd, fun _ _ => rfl⟩

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