no goals
M : Type u_2
N : Type ?u.1812
P : Type ?u.1815
E : Type ?u.1818
α✝ : Type ?u.1821
β : Type u_3
inst✝⁶ : SMul M α✝
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α✝
inst✝³ : SMul N β
a✝ : M
x : α✝ × β
α : Type u_1
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)
rw [Prod.smul_mk, smul_zero]