English
There is an equivalence between DistribMulAction on M × N and the combined data of commuting actions of M and N on α.
Русский
Существует эквивариантность между DistribMulAction на M × N и объединёнными данными коммутирующих действий M и N на α.
LaTeX
$$$\\text{DistribMulAction}(M \\times N) \\alpha \\cong \\Sigma'(\\text{DistribMulAction } M \\alpha) (\\text{DistribMulAction } N \\alpha), \\text{SMulCommClass } M N \\alpha$$$
Lean4
/-- Construct a `DistribMulAction` by a product monoid from `DistribMulAction`s by the factors. -/
abbrev prodOfSMulCommClass [DistribMulAction M α] [DistribMulAction N α] [SMulCommClass M N α] :
DistribMulAction (M × N) α where
__ := MulAction.prodOfSMulCommClass M N α
smul_zero mn := by change mn.1 • mn.2 • 0 = (0 : α); rw [smul_zero, smul_zero]
smul_add mn a a' := by change mn.1 • mn.2 • _ = (_ : α); rw [smul_add, smul_add]; rfl
