mathlib3

f23a09ce - feat(analysis/special_functions/log/base): add `real.logb_mul_base` (#18979)

feat(analysis/special_functions/log/base): add `real.logb_mul_base` (#18979) Add proof that states `logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>