English
Let M and M₂ be modules over a semiring R. The map that sends (m, n) ∈ M × M₂ to m ∈ M is a linear map from M × M₂ to M.
Русский
Пусть M и M₂ — модули над полем/кольцом R. Отображение, отправляющее (m, m₂) ∈ M × M₂ в m ∈ M, является линейным отображением M × M₂ → M.
LaTeX
$$$\\pi_1: M \\times M_2 \\to M$, $\\pi_1(m,n)=m$, и $\\pi_1((m_1,n_1)+(m_2,n_2))=m_1+m_2$, $\\pi_1(r(m,n))=r\\,m$ for all $m,m_1,m_2\\in M$, $n,n_1,n_2\\in M_2$, $r\\in R$.$$
Lean4
/-- The first projection of a product is a linear map. -/
def fst : M × M₂ →ₗ[R] M where
toFun := Prod.fst
map_add' _x _y := rfl
map_smul' _x _y := rfl
