fst — Mathlib

English

The first projection from A × B to A is a nonunital algebra homomorphism.

Русский

Первая проекция из A × B в A является неполунальным алгебра-гомоморфизмом.

LaTeX

$$$\text{fst}: A \times B \to_{R} A$ is the projection to the first coordinate, i.e. $\text{fst}(a,b)=a$.$$

Lean4

/-- The first projection of a product is a non-unital algebra homomorphism. -/
@[simps]
def fst : A × B →ₙₐ[R] A where
  toFun := Prod.fst
  map_zero' := rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  map_mul' _ _ := rfl

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