English
Let M and N be sets equipped with a binary operation (i.e., semigroups). Then the Cartesian product M × N carries a natural binary operation defined coordinatewise by (m1, n1) · (m2, n2) = (m1 · m2, n1 · n2); in particular, M × N forms a semigroup under this operation.
Русский
Пусть M и N — множества, имеющие двоичную операцию умножения (полугруппы). Тогда декартово произведение M × N оснащается естественной бинарной операцией
(м1, н1) · (м2, н2) = (м1 · м2, н1 · н2); следовательно, произведение M × N образует полугруппу при такой операции.
LaTeX
$$$\forall M,N\; (\operatorname{Mul} M \land \operatorname{Mul} N) \Rightarrow \operatorname{Mul}(M \times N), \quad (m_1,m_2) \cdot (n_1,n_2) = (m_1 n_1, m_2 n_2)$$$
Lean4
@[to_additive]
instance instMul : Mul (M × N) :=
⟨fun p q => ⟨p.1 * q.1, p.2 * q.2⟩⟩
