lean_workbook_plus_42799

Proved

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

Vieta's gives that $\frac{m_k}{18} = 2 \iff m_k = 36$ . We now have $36 = 6f + 9g$ . Taking it $\pmod{6}$ we get $0 \equiv 3g \pmod{6} \iff g\in\{0,2,4\}$ . Taking it $\pmod{9}$ we get $0\equiv6f\pmod{9}\iff f\in\{0,3,6\}$ . Thus, $(f,g)\in \{(0,4),(3,2),(6,0)\}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42799  (f g : ℕ)
  (h₀ : 0 < f ∧ 0 < g)
  (h₁ : 6 * f + 9 * g = 36) :
  (f, g) = (3, 2) ∨ (f, g) = (6, 0) ∨ (f, g) = (0, 4)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph