Mathlib's log and Core's log

Stream: Is there code for X?

[Tomaz Mascarenhas]

Is there a proof somewhere that the logarithm defined in mathlib is equal to log2 defined in core?

Mathlib's log: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Log.lean#L41

Core's log2: https://github.com/leanprover/lean4/blob/master/src/Init/Data/Nat/Log2.lean

[Markus Himmel]

(deleted)

[Markus Himmel]

@loogle Nat.log, Nat.log2

[loogle]

:search: Nat.log2_eq_log_two

[Tomaz Mascarenhas]

oh, thank you!