Prove2Me

Adding exponents of a positive real base

Proved
WorkbookRestored.plus_8562

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For real a,x,ya,x,y with a>0a>0,

axay=ax+y.a^x a^y=a^{x+y}.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_8562 (Apache-2.0).

Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Base
open Real
Formal statement
theorem WorkbookRestored.plus_8562 (a x y : ℝ) (ha : 0 < a) : a^x * a^y = a^(x + y)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_8562; original Prove2Me node 46ff52ca-112b-4973-bfdb-2df4af04c685; Apache-2.0

View graph