fst — Mathlib

English

For semirings R,S, the projection fst : R × S → R is surjective; there exists a right inverse sending r to (r,0).

Русский

Для полорых R,S отображение fst: R×S → R сюръективно; существует правый обратный, отправляющий r в (r,0).

LaTeX

$$$\\text{fst}: R \\times S \\to R \\text{ is surjective, with } r \\mapsto (r,0).$$$

Lean4

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

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