Commit 2024-04-15 10:00 7700a474

View on Github →

Feat(Log/Base): Adding 3 theorems related to Real.logb (#12110)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/Base.lean

added theorem Real.logb_eq_iff_rpow_eq

added theorem Real.logb_pow

added theorem Real.logb_rpow_eq_mul_logb_of_pos