lean_workbook_plus_38318
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38318 (x y m n : ℤ) (h : 2017 ∣ y^2*m^2 - x^2*n^2) : 2017 ∣ (y*m - x*n)*(y*m + x*n) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38318 (x y m n : ℤ) (h : 2017 ∣ y^2*m^2 - x^2*n^2) : 2017 ∣ (y*m - x*n)*(y*m + x*n) := by sorry