snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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