Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-01 00:08 b52cb02c

View on Github →

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.

Estimated changes

modified theorem real.log_le_log
added theorem real.log_div_log
added theorem real.logb_abs
added theorem real.logb_div
added theorem real.logb_eq_zero
added theorem real.logb_inj_on_pos
added theorem real.logb_inv
added theorem real.logb_le_logb
added theorem real.logb_lt_logb
added theorem real.logb_lt_logb_iff
added theorem real.logb_mul
added theorem real.logb_neg
added theorem real.logb_neg_eq_logb
added theorem real.logb_neg_iff
added theorem real.logb_nonneg
added theorem real.logb_nonneg_iff
added theorem real.logb_nonpos
added theorem real.logb_nonpos_iff'
added theorem real.logb_nonpos_iff
added theorem real.logb_one
added theorem real.logb_pos
added theorem real.logb_pos_iff
added theorem real.logb_prod
added theorem real.logb_rpow
added theorem real.logb_surjective
added theorem real.logb_zero
added theorem real.range_logb
added theorem real.rpow_logb
added theorem real.rpow_logb_eq_abs
added theorem real.rpow_logb_of_neg
added theorem real.surj_on_logb'
added theorem real.surj_on_logb