The ℕ/ℤ-cast inner-product smul lemmas formerly in this file are now covered by mathlib's inner_smul_left_eq_smul and inner_smul_right_eq_smul (general over any scalar tower).