Documentation

PFR.Mathlib.Analysis.SpecialFunctions.Log.Basic

source
@[simp]
theorem Real.log_div_self (x : ℝ) :
Real.log (x / x) = 0