lean_workbook_plus_67110

Proved

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

Given $g(xy)=g(x)g(y)$ and $g(2)=4$ , find $g(4)$ and $g(16)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67110 (g : ℝ → ℝ) (h₁ : ∀ x y, g (x*y) = g x * g y) (h₂ : g 2 = 4) : g 4 = 16 ∧ g 16 = 256   :=  by sorry

Source