theorem wss_vec3_generic {k : Type u_1} [CommSemiring k] (w₀ w₁ w₂ x₀ x₁ x₂ : k) : (QuadraticMap.weightedSumSquares k ![w₀, w₁, w₂]) ![x₀, x₁, x₂] = w₀ * (x₀ * x₀) + w₁ * (x₁ * x₁) + w₂ * (x₂ * x₂)

Generic expansion of the 3-variable weighted sum of squares over any commutative semiring $k$.

theorem wss_vec3 (w₀ w₁ w₂ x₀ x₁ x₂ : ℝ) : (QuadraticMap.weightedSumSquares ℝ ![w₀, w₁, w₂]) ![x₀, x₁, x₂] = w₀ * (x₀ * x₀) + w₁ * (x₁ * x₁) + w₂ * (x₂ * x₂)

Specialization of wss_vec3_generic to the real numbers.

theorem vec3_ne_zero_of_idx0 {α : Type u_1} [Zero α] (a b c : α) (ha : a ≠ 0) : ![a, b, c] ≠ 0

The triple $[a, b, c]$ is nonzero if its first component is.

theorem vec3_ne_zero_of_idx1 {α : Type u_1} [Zero α] (a b c : α) (hb : b ≠ 0) : ![a, b, c] ≠ 0

The triple $[a, b, c]$ is nonzero if its second component is.

theorem vec3_ne_zero_of_idx2 {α : Type u_1} [Zero α] (a b c : α) (hc : c ≠ 0) : ![a, b, c] ≠ 0

The triple $[a, b, c]$ is nonzero if its third component is.