ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4828 on D866: Standard real logarithm function
Logarithm of one is zero