smul_zero_mk — Mathlib

English

Let M act on α and β componentwise on the product α × β. Then for every a ∈ M and every c ∈ β, we have a · ((0, c)) = (0, a · c).

Русский

Пусть M действует на α и β по произведению α × β по координатам. Тогда для любого a ∈ M и любого c ∈ β выполнено: a · ((0, c)) = (0, a · c).

LaTeX

$$$a \\cdot ((0 : \\alpha), c) = (0, a \\cdot c)$$$

Lean4

theorem smul_zero_mk {α : Type*} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) :
    a • ((0 : α), c) = (0, a • c) := by rw [Prod.smul_mk, smul_zero]

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