Theorems · Theorem · field theory
Finset.sum_div
∀ {ι : Type u_1} {K : Type u_2} [inst : DivisionSemiring K] (s : Finset ι) (f : ι → K) (a : K),
(∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a- Defined in
- Mathlib.Algebra.BigOperators.Field
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionSemiring
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.
- Finsetstatement and proof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Finset.sum_congrproof · cited by 2,323
- div_eq_mul_invproof · cited by 715
- DivisionSemiringstatement and proof · cited by 216
- Finset.sum_mulproof · cited by 112
Cited by20
Results whose statement or proof uses this declaration.
- ProbabilityTheory.iIndepFun.hasGaussianLawproof · cited by 3
- NumberField.Ideal.tendsto_norm_le_div_atTop₀proof · cited by 2
- LSeries.term_sum_applyproof · cited by 2
- GaussianFourier.integral_cexp_neg_mul_sum_addproof · cited by 1
- LSeries.term_convolutionproof · cited by 1
- ENNReal.lintegral_prod_norm_pow_leproof · cited by 1
- inner_sum_smul_sum_smul_of_sum_eq_zeroproof · cited by 1
- bernstein.varianceproof · cited by 1
- ZMod.LFunction_eq_completed_div_gammaFactor_evenproof · cited by 1
- ZMod.LFunction_eq_completed_div_gammaFactor_oddproof · cited by 1
- BoxIntegral.unitPartition.integralSum_eq_tsum_divproof · cited by 1
- IsVisible.of_convexHull_of_posproof · cited by 1