Theorem: ListN.mul_elemwise (SciLean/Data/ListN.lean)

State before:
α : Type u_1
n : Nat
inst✝ : Mul α
x y : α
xs ys : ListN α n
⊢ cons x xs * cons y ys = cons (x * y) (xs * ys)
Tactic:
rfl
State after:
no goals