lean_workbook_plus_20139
OpenProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20139 : ∀ x y : ℝ, x > 0 ∧ y > 0 → Real.log x + Real.log y = Real.log (x*y) := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20139 : ∀ x y : ℝ, x > 0 ∧ y > 0 → Real.log x + Real.log y = Real.log (x*y) := by sorry