Prove2Me

Exponent_Combination_Laws

Proved

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

analysisexponentsproofwikireal-analysis

For a > 0 and real x, y: a^(x+y) = a^x * a^y.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

theorem Exponent_Combination_Laws (a : ℝ) (ha : 0 < a) (x y : ℝ) : a ^ (x + y) = a ^ x * a ^ y := by sorry
Source
https://proofwiki.org/wiki/Exponent_Combination_Laws

View graph