Theorems · Theorem · measure theory
intervalIntegral.integral_mul_const
∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_8} [inst : RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜),
∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r- Cited by
- 4 results in Mathlib
- Foundations
- Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RCLike
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.Measurestatement and proof · cited by 10,939
- RCLikestatement and proof · cited by 2,829
- mul_commproof · cited by 2,262
- intervalIntegralstatement and proof · cited by 546
- intervalIntegral.integral_const_mulproof · cited by 29
Cited by4
Results whose statement or proof uses this declaration.
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- intervalIntegral.integral_divproof · cited by 3
- ODE.FunSpace.dist_iterate_next_apply_leproof · cited by 1
- sum_Ico_pow_mul_exp_neg_leproof · cited by 1