smulZeroClass — Mathlib

English

If R acts with zero on M and N, then R acts with zero on M × N by componentwise action, i.e., r · (0,0) = (0,0) for all r ∈ R.

Русский

Если R действует с нулём на M и N, то R действует на произведение M × N с нулём по компонентам, то есть для любого r ∈ R выполняется r · (0,0) = (0,0).

LaTeX

$$$r \\cdot (0,0) = (0,0)$$$

Lean4

instance smulZeroClass {R M N : Type*} [Zero M] [Zero N] [SMulZeroClass R M] [SMulZeroClass R N] :
    SMulZeroClass R (M × N) where smul_zero _ := by ext <;> exact smul_zero _

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