Theorems · Theorem · real analysis
Frullani.integral_comp_mul_inv_smul
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c ε r : ℝ},
c ≠ 0 → ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x- Cited by
- 1 results in Mathlib
- Foundations
- Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- one_mulproof · cited by 2,841
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- one_ne_zeroproof · cited by 885
- div_oneproof · cited by 629
- intervalIntegralstatement and proof · cited by 546
- smul_smulproof · cited by 360
- intervalIntegral.integral_smulproof · cited by 10
- intervalIntegral.smul_integral_comp_mul_leftproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Frullani.tendsto_intervalIntegralproof · cited by 1