theorem InnerProductSpace.natCast_smul_left {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} {a : ℕ} : inner 𝕜 (a • u) v = a • inner 𝕜 u v

theorem InnerProductSpace.intCast_smul_left {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} {a : ℤ} : inner 𝕜 (a • u) v = a • inner 𝕜 u v

theorem InnerProductSpace.natCast_smul_right {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} {a : ℕ} : inner 𝕜 u (a • v) = a • inner 𝕜 u v

theorem InnerProductSpace.intCast_smul_right {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} {a : ℤ} : inner 𝕜 u (a • v) = a • inner 𝕜 u v