Theorems · Definition · real analysis
Real.logb
ℝ → ℝ → ℝ
The real logarithm in a given base. As with the natural logarithm, we define logb b x to
be logb b |x| for x < 0, and 0 for x = 0.
- Cited by
- 119 results in Mathlib
- Foundations
- Depth 169 from the axioms, rests on 4,684 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by119
Results whose statement or proof uses this declaration.
- Real.rpow_logbstatement · cited by 15
- Real.logb_onestatement · cited by 7
- Real.logb_rpowstatement · cited by 5
- Real.logb_zerostatement · cited by 5
- Real.logb_nonnegstatement · cited by 4
- Real.logb_absstatement and proof · cited by 3
- Real.logb_one_leftstatement · cited by 3
- Real.logb_zero_leftstatement · cited by 3
- Real.floor_logb_natCaststatement and proof · cited by 2
- Real.rpow_logb_eq_absstatement and proof · cited by 2
- Real.logb_le_logbstatement and proof · cited by 2
- Real.logb_lt_logbstatement and proof · cited by 2