lean_workbook_plus_19865
ProvedIf and then or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19865 (x y z : ℝ) (h : x^3 + y^3 + z^3 = 3 * x * y * z) : x + y + z = 0 ∨ x = y ∧ y = z := by sorry
Source
If and then or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19865 (x y z : ℝ) (h : x^3 + y^3 + z^3 = 3 * x * y * z) : x + y + z = 0 ∨ x = y ∧ y = z := by sorry