lean_workbook_plus_69515

Proved

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

Given a function $f(x)$ such that $f(x+y) = f(x) \cdot f(y)$ and $f(1) = \frac{1}{2}$ , find $f(n)$ for $n \in \mathbb{N}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69515 (f : ℕ → ℝ) (n : ℕ) (h₁ : f 1 = 1/2) (h₂ : ∀ x y : ℕ, f (x + y) = f x * f y) : f n = (1/2)^n   :=  by sorry

Source