mathlib3

b52cb02c - feat(analysis/special_functions/{log, pow}): add log_base (#11246)

feat(analysis/special_functions/{log, pow}): add log_base (#11246) Adds `real.logb`, the log base `b` of `x`, defined as `log x / log b`. Proves that this is related to `real.rpow`.