real.log in other base

Stream: Is there code for X?

[Kunhao Zheng]

Hello! I am now writing some exercises like ( ( 5 ^ 2 ) logb ( 5 ^ 4 ) ) = 2 (which means that logarithm of 5^4 in base 5^2 is 2).
I would like to know if there is already a way to write logarithm in this way in Lean (seems like I didn't find it in real.log), or I need write a simple function which takes 2 arguments to define this logb. Thank you in advance!

[Mario Carneiro]

You would need to write a function for this. I don't think logb is defined in lean, although it's not hard: logb b x = log x / log b

[Mario Carneiro]

so in lean that would look like

import analysis.special_functions.exp_log

namespace real

noncomputable def logb (b x : ℝ) : ℝ := log x / log b

example : logb (5^2) (5^4) = 2 := sorry

end real

[Mario Carneiro]

(also, fancy meeting you here, I can see you've been writing metamath from the spaces :grinning_face_with_smiling_eyes:)

[Kunhao Zheng]

Thank you for this so concrete example @Mario Carneiro ! Aha it is the grammar of metamath :grinning:

[Bolton Bailey]

Has this been implemented yet? Edit: I PR'd it.