lean_workbook_plus_82433

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find $m^2+4n^2$ given $m^3-12mn^2=40$ and $4n^3-3m^2n=10$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82433 (m n : ℤ) (h1 : m^3 - 12*m*n^2 = 40) (h2 : 4*n^3 - 3*m^2*n = 10) : m^2 + 4*n^2 = 14   :=  by sorry

Source