Theorems · Theorem · measure theory
Real.circleAverage_smul
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} [inst_2 : NormedDivisionRing 𝕜]
[inst_3 : Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] {f : ℂ → E} {c : ℂ} {R : ℝ} {a : 𝕜},
Real.circleAverage (a • f) c R = a • Real.circleAverage f c RCircle averages commute with scalar multiplication.
- Cited by
- 1 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.
Cites17
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
- Modulestatement and proof · cited by 20,661
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Complexstatement and proof · cited by 5,565
- SMulCommClassstatement and proof · cited by 1,927
- Real.piproof · cited by 1,774
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- intervalIntegralproof · cited by 546
- NormedDivisionRingstatement and proof · cited by 360
- mul_inv_revproof · cited by 270
- SMulCommClass.smul_commproof · cited by 143
Cited by1
Results whose statement or proof uses this declaration.
- Real.circleAverage_fun_smulproof · cited by 2