mulDistribMulAction — Mathlib

English

The product M × N has a SMulWithZero structure: for any r, r · (0,0) = (0,0).

Русский

Произведение M × N имеет структуру SMulWithZero: для любого r выполняется r · (0,0) = (0,0).

LaTeX

$$$a \\cdot ((0 : M), (0 : N)) = (0,0)$$$

Lean4

instance mulDistribMulAction {R : Type*} [Monoid R] [Monoid M] [Monoid N] [MulDistribMulAction R M]
    [MulDistribMulAction R N] : MulDistribMulAction R (M × N)
    where
  smul_mul _ _ _ := by ext <;> exact smul_mul' ..
  smul_one _ := by ext <;> exact smul_one _

Похожие утверждения