lean_workbook_plus_19076

Open

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

Examples: $a=e$ , $b=\ln(2)$ , $\Rightarrow$ ${a^b} = {e^{\ln (2)}} = 2 \in \mathbb{Q}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19076 (a b : ℝ) (ha : a = Real.exp 1) (hb : b = Real.log 2) : a^b = 2   :=  by sorry

Source