English
The product M × N carries a natural A-module structure: addition and scalar multiplication are defined componentwise: (m1,n1)+(m2,n2)=(m1+m2,n1+n2) and a·(m,n)=(a·m,a·n).
Русский
Произведение M × N естественным образом является модулем над A: сложение и умножение на скаляр выполняются по каждому компоненту: (m1,n1)+(m2,n2)=(m1+m2,n1+n2), a·(m,n)=(a·m,a·n).
LaTeX
$$$$ (M \\times N) \\text{ is an } A\\text{-module with } (m_1,n_1)+(m_2,n_2)=(m_1+m_2,n_1+n_2),\\ a\\cdot(m,n)=(a\\cdot m,a\\cdot n). $$$$
Lean4
instance instModule [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Module R (M × N)
where
add_smul _ _ _ := by ext <;> exact add_smul ..
zero_smul _ := by ext <;> exact zero_smul ..
