Prove2Me

Exponential_of_Product

Proved

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

analysisexponentialproofwikireal-analysis

For real numbers x, y: exp(xy) = exp(y)^x.

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 Exponential_of_Product (x y : ℝ) : Real.exp (x * y) = (Real.exp y) ^ x := by sorry
Source
https://proofwiki.org/wiki/Exponential_of_Product

View graph