lean_workbook_plus_19421

Disproved

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

$(1+\frac{1}{a})(1+\frac{1}{b})(1+\frac{1}{c})=1+\frac{1}{a}+\frac{1}{b}+\frac{1}{c}+\frac{2}{abc}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19421 : ∀ a b c : ℝ, (1 + 1 / a) * (1 + 1 / b) * (1 + 1 / c) = 1 + 1 / a + 1 / b + 1 / c + 2 / (a * b * c)   :=  by sorry

Source