Entry	Value
Package Name	natural-exp-log-def
Count	1
Theorems	log_def : !k n m. k EXP m <= n /\ n < k EXP (m + 1) ==> log k n = m

Back to main package page