snd — Mathlib

English

The map snd : R × S → S is a ring homomorphism sending (a,b) to b.

Русский

Отображение snd : R × S → S является гомоморфизмом колец и отправляет (a,b) в b.

LaTeX

$$$\\text{snd}: R \\times S \\to S \\text{ is a ring homomorphism with } \\text{snd}(a,b)=b.$$$

Lean4

/-- Given non-unital semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`. -/
def snd : R × S →ₙ+* S :=
  { MulHom.snd R S, AddMonoidHom.snd R S with toFun := Prod.snd }

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