Theorems · Theorem · ring theory
Nat.cast_sum
∀ {R : Type u_4} {ι : Type u_5} [inst : AddCommMonoidWithOne R] (s : Finset ι) (f : ι → ℕ),
↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)- Defined in
- Mathlib.Algebra.BigOperators.Ring.Finset
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoidWithOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 5,195
- map_sumproof · cited by 455
- AddCommMonoidWithOnestatement and proof · cited by 42
- Nat.castAddMonoidHomproof · cited by 16
Cited by38
Results whose statement or proof uses this declaration.
- IsPGroup.card_modEq_card_fixedPointsproof · cited by 4
- AddSubgroup.leftCoset_cover_filter_FiniteIndex_auxproof · cited by 3
- catalan_eq_centralBinom_divproof · cited by 3
- Subgroup.leftCoset_cover_filter_FiniteIndex_auxproof · cited by 3
- NumberField.Ideal.tendsto_norm_le_div_atTop₀proof · cited by 2
- NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_leproof · cited by 2
- Chebyshev.primeCounting_eq_theta_div_log_add_integralproof · cited by 2
- Nat.Prime.emultiplicity_choose'proof · cited by 2
- tsum_prod_pow_eq_tsum_sigmaproof · cited by 2
- char_dvd_card_solutions_of_sum_ltproof · cited by 2
- PairReduction.card_pairSet_leproof · cited by 1