snd — Mathlib

English

Let M and M₂ be modules over a semiring R. The map that sends (m, n) to n is linear, i.e., defines a linear map from M × M₂ to M₂.

Русский

Пусть M и M₂ — модули над кольцом R. Отображение, отправляющее (m, m₂) в m₂, линейно.

LaTeX

$$$\\pi_2: M \\times M_2 \\to M_2$, $\\pi_2(m,n)=n$, and $\\pi_2((m_1,n_1)+(m_2,n_2))=n_1+n_2$, $\\pi_2(r(m,n))=r\\,n$.$$

Lean4

/-- The second projection of a product is a linear map. -/
def snd : M × M₂ →ₗ[R] M₂ where
  toFun := Prod.snd
  map_add' _x _y := rfl
  map_smul' _x _y := rfl

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