Theorems · Theorem · real analysis
integral_pow
∀ {a b : ℝ} (n : ℕ), ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)- Cited by
- 8 results in Mathlib
- Foundations
- Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- intervalIntegralstatement and proof · cited by 546
- zpow_natCastproof · cited by 271
- Nat.cast_nonnegproof · cited by 109
- integral_zpowproof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- integral_idproof · cited by 2
- integral_pow_abs_sub_uIocproof · cited by 1
- MeasureTheory.Measure.volumeIoiPow_apply_Iioproof · cited by 1
- integral_cos_pow_threeproof · cited by 0
- integral_sin_mul_cos_sqproof · cited by 0
- integral_sin_pow_threeproof · cited by 0
- integral_sin_sq_mul_cosproof · cited by 0