Prove2Me

Sum_of_Logarithms

Proved

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

analysislogarithmproofwikireal-analysis

For positive reals x, y: log(xy) = log(x) + log(y).

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic

theorem Sum_of_Logarithms (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : Real.log (x * y) = Real.log x + Real.log y := by sorry
Source
https://proofwiki.org/wiki/Sum_of_Logarithms

View graph