lean_workbook_plus_2836
ProvedProve that if , then for all
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2836 (n : ℕ) (x : Fin n → ℝ) (h : ∑ i, x i ^ 2 = 0) : ∀ i, x i = 0 := by sorry
Source
Prove that if , then for all
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2836 (n : ℕ) (x : Fin n → ℝ) (h : ∑ i, x i ^ 2 = 0) : ∀ i, x i = 0 := by sorry