lean_workbook_plus_28764
ProvedIndeed, implies .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28764 (n : ℕ) (x : Fin n → ℝ) (hx : ∑ i, x i ^ 2 = 0) : ∀ i, x i = 0 := by sorry
Source
Indeed, implies .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28764 (n : ℕ) (x : Fin n → ℝ) (hx : ∑ i, x i ^ 2 = 0) : ∀ i, x i = 0 := by sorry