Theorem: shape_prod_nil (MLIR/Util/KDTensor.lean)

State before:
l : List ℕ
⊢ shapeProd (0 :: l) = 0
Tactic:
induction l <;> simp [shapeProd, List.foldr]
State after:
no goals