lean_workbook_plus_66830

Proved

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

Solve the system of equations [1] and [2]:\n\n $6a_1 + a_2 = -27 \quad [1]$ \n\n $3a_1 + 2a_2 = -2 \quad [2]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66830 (a₁ a₂ : ℝ) : (6*a₁ + a₂ = -27 ∧ 3*a₁ + 2*a₂ = -2) ↔ a₁ = -52/9 ∧ a₂ = 23/3   :=  by sorry

Source