Theorems · Theorem · measure theory
MeasureTheory.Integrable.div_const
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedDivisionRing 𝕜]
{f : α → 𝕜}, MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x / c) μ- Cited by
- 4 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedDivisionRing
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.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- div_eq_mul_invproof · cited by 715
- NormedDivisionRingstatement and proof · cited by 360
- MeasureTheory.Integrable.mul_constproof · cited by 17
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.tilted_apply_eq_ofReal_integralproof · cited by 1
- MeasureTheory.tilted_apply_eq_ofReal_integral'proof · cited by 1
- ContDiffBump.integrable_normedproof · cited by 0
- MellinConvergent.div_constproof · cited by 0