English
Let M be a monoid acting on two sets α and β. Then α × β carries the natural product action of M, defined by m · (a, b) = (m · a, m · b). This action satisfies the usual action axioms: (1) 1 · (a, b) = (a, b) and (mn) · (a, b) = m · (n · (a, b)).
Русский
Пусть M — моноид, действующий на множества α и β. Тогда произведение α × β наделяется естественным произведением действия M, заданным как m · (a, b) = (m · a, m · b). Это действие удовлетворяет обычным аксиомам действия: 1 · (a, b) = (a, b) и (mn) · (a, b) = m · (n · (a, b)).
LaTeX
$$$\text{MulAction } M (\alpha \times \beta) \text{ with } m \cdot (a,b) = (m \cdot a, m \cdot b),\; 1\cdot(a,b)=(a,b),\; (m_1m_2)\cdot(a,b)=m_1\cdot(m_2\cdot(a,b)).$$$
Lean4
@[to_additive]
instance mulAction [Monoid M] [MulAction M α] [MulAction M β] : MulAction M (α × β)
where
mul_smul _ _ _ := by ext <;> exact mul_smul ..
one_smul _ := by ext <;> exact one_smul ..
