lean_workbook_plus_8957

Proved

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

Given $k=a+b+c$ , let $a_{1}=\frac{a}{k}$ , $b_{1}=\frac{b}{k}$ , $c_{1}=\frac{c}{k}$ . Show that $a_{1}+b_{1}+c_{1}=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8957 (a b c k : ℝ) (h₁ : k = a + b + c) (h₂ : a + b + c ≠ 0) : a / k + b / k + c / k = 1   :=  by sorry

Source