lean_workbook_plus_64826
ProvedWhen . Then we have,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64826 (x y z : ℝ) (h : x + y = 0 ∧ y + z = 0 ∧ z + x = 0) : x = 0 ∧ y = 0 ∧ z = 0 := by sorry
Source
When . Then we have,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64826 (x y z : ℝ) (h : x + y = 0 ∧ y + z = 0 ∧ z + x = 0) : x = 0 ∧ y = 0 ∧ z = 0 := by sorry