lean_workbook_plus_13969

Proved

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

Find $c_{1}y_{1}+c_{2}y_{2}$ where $y_{1}= \frac{5x-6}{25}$ , $y_{2}= \frac{5x-6}{25}$ , $c_{1}=-1$ , and $c_{2}= 1$ . Is $-1\cdot y_{1}+1\cdot y_{2}= 0$ a solution?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13969 (x : ℝ) : (-1 * (5 * x - 6) / 25) + (1 * (5 * x - 6) / 25) = 0   :=  by sorry

Source

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

View graph