fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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