Theorem: MProd.smul_mk (SciLean/Core/Monads/MProd.lean)

State before:
K : Type u_1
X Y : Type u_2
inst✝¹ : SMul K X
inst✝ : SMul K Y
k : K
x : X
y : Y
⊢ k • { fst := x, snd := y } = { fst := k • x, snd := k • y }
Tactic:
rfl
State after:
no goals