lean_workbook_plus_79039
ProvedGiven and , show that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79039 (a b p q : ℕ) : a = p * q + p ^ 2 ∧ b = p * q + q ^ 2 → √(a + b) = p + q := by sorry
Source
Given and , show that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_79039 (a b p q : ℕ) : a = p * q + p ^ 2 ∧ b = p * q + q ^ 2 → √(a + b) = p + q := by sorry