lean_workbook_plus_47115

Proved

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

Prove that if x and y are rational numbers and k is irrational, then $x+ky=0 \implies x=y=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47115 (x y : ℚ) (k : ℝ) (h₁ : x + k * y = 0) (h₂ : ¬ k ∈ Set.range ((↑) : ℚ → ℝ)) : x = 0 ∧ y = 0   :=  by sorry

Source