no goals
M : Type u_2
N : Type ?u.3133
P : Type ?u.3136
E : Type ?u.3139
α : Type u_3
β✝ : Type ?u.3145
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
b : α
⊢ a • (b, 0) = (a • b, 0)
rw [Prod.smul_mk, smul_zero]