English
If M and N act on α and the actions commute (SMulCommClass M N α), then there is a MulAction of the product M × N on α defined by (m, n) · a = m · n · a. The action satisfies the unit and associativity laws thanks to the commutation assumption.
Русский
Если M и N действуют на α и их действия коммютируют (SMulCommClass M N α), то существует MulAction произведения M × N на α, заданное (m, n) · a = m · n · a. Элементарные свойства действия выполняются благодаря условию коммутативности.
LaTeX
$$$\text{MulAction } (M \times N) \alpha \text{ with } (m,n) \cdot a = m \cdot n \cdot a,\; 1 \cdot a = a,\; (x,y) \cdot (x',y') \cdot a = x \cdot y \cdot x' \cdot y' \cdot a$ with appropriate rearrangements via commutativity.$$
Lean4
/-- Construct a `MulAction` by a product monoid from `MulAction`s by the factors.
This is not an instance to avoid diamonds for example when `α := M × N`. -/
@[to_additive AddAction.prodOfVAddCommClass /--
Construct an `AddAction` by a product monoid from `AddAction`s by the factors.
This is not an instance to avoid diamonds for example when `α := M × N`. -/
]
abbrev prodOfSMulCommClass [MulAction M α] [MulAction N α] [SMulCommClass M N α] : MulAction (M × N) α
where
smul mn a := mn.1 • mn.2 • a
one_smul a := (one_smul M _).trans (one_smul N a)
mul_smul x y
a := by
change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
rw [mul_smul, mul_smul, smul_comm y.1 x.2]
