Factoring a homogeneous quadratic equation over the complex numbers
ProvedWorkbookSource.problem_41226lean-workbooksource-checked
For complex x,y, 2x²−3xy+y²=0 if and only if (x−y)(2x−y)=0.
Source: InternLM Lean-Workbook, record lean_workbook_41226 (Apache-2.0). The complete source proposition and variable types are retained.
Preamble
import Mathlib open Complex
Formal statement
theorem WorkbookSource.problem_41226 : ∀ x y : ℂ, (2 * x ^ 2 - 3 * x * y + y ^ 2 = 0) ↔ (x - y) * (2 * x - y) = 0 := by sorry
Source