lean_workbook_plus_38975
Proved.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38975 (m n : ℤ) (h : m ≠ n) (h2 : m^2 + m*n + n^2 = 1) : m^3 - n^3 = m - n := by sorry
Source
.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38975 (m n : ℤ) (h : m ≠ n) (h2 : m^2 + m*n + n^2 = 1) : m^3 - n^3 = m - n := by sorry