Theorems · Theorem · measure theory
intervalIntegral.integral_const_mul
∀ {𝕜 : Type u_2} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜]
(r : 𝕜) (f : ℝ → 𝕜), ∫ (x : ℝ) in a..b, r * f x ∂μ = r * ∫ (x : ℝ) in a..b, f x ∂μ- Cited by
- 29 results in Mathlib
- Foundations
- Depth 254 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.Measurestatement and proof · cited by 10,939
- NormedAlgebrastatement and proof · cited by 1,165
- intervalIntegralstatement · cited by 546
- NormedDivisionRingstatement and proof · cited by 360
- intervalIntegral.integral_smulproof · cited by 10
Cited by29
Results whose statement or proof uses this declaration.
- intervalIntegral.integral_mul_constproof · cited by 4
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- qExpansion_coeff_isBigO_of_norm_isBigOproof · cited by 2
- Chebyshev.integral_theta_div_log_sq_isBigOproof · cited by 2
- integral_inv_sq_add_sqproof · cited by 1
- GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_Iproof · cited by 1
- ValueDistribution.circleAverage_circleAverage_eq_proximity_topproof · cited by 1
- ODE.FunSpace.dist_iterate_next_apply_leproof · cited by 1
- Complex.GammaSeq_eq_approx_Gamma_integralproof · cited by 1
- ZetaAsymptotics.term_of_ltproof · cited by 1
- ZetaAsymptotics.term_oneproof · cited by 1
- MeasureTheory.integral_charFun_Iccproof · cited by 1