Properties_of_Natural_Logarithm
Provedanalysislogarithmproofwikireal-analysis
Properties of ln: ln(1) = 0, and ln(xy) = ln(x) + ln(y) for positive reals.
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 Properties_of_Natural_Logarithm : Real.log 1 = 0 ∧ ∀ x y : ℝ, 0 < x → 0 < y → Real.log (x * y) = Real.log x + Real.log y := by sorry
Source