Theorems · Theorem · real analysis
Real.log_nat_eq_sum_factorization
∀ (n : ℕ), Real.log ↑n = n.factorization.sum fun p t => ↑t * Real.log ↑p
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- eq_or_neproof · cited by 1,117
- Real.logstatement and proof · cited by 939
- Finsupp.sumstatement and proof · cited by 481
- CharP.cast_eq_zeroproof · cited by 357
- Nat.factorizationstatement and proof · cited by 215
- Real.log_zeroproof · cited by 84
- Nat.factorization_zeroproof · cited by 32
- eq_zero_of_pow_eq_zeroproof · cited by 30
- Nat.prod_factorization_pow_eq_selfproof · cited by 22
- Nat.cast_eq_zeroproof · cited by 18
Cited by1
Results whose statement or proof uses this declaration.
- Real.logb_nat_eq_sum_factorizationproof · cited by 0