Factoring a polynomial in a product of complex variables
ProvedWorkbookSource.problem_47631lean-workbooksource-checked
For complex b,z, z²b²+zb−2=(bz−1)(bz+2).
Source: InternLM Lean-Workbook, record lean_workbook_47631 (Apache-2.0). The complete source proposition and variable types are retained.
Preamble
import Mathlib open Complex
Formal statement
theorem WorkbookSource.problem_47631 : ∀ b z:ℂ, z^2 * b^2 + z * b - 2 = (b * z - 1) * (b * z + 2) := by sorry
Source