Theorems · Theorem · ring theory
Int.cast_sum
∀ {R : Type u_4} {ι : Type u_5} [inst : AddCommGroupWithOne R] (s : Finset ι) (f : ι → ℤ),
↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)- Defined in
- Mathlib.Algebra.BigOperators.Ring.Finset
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommGroupWithOne
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
- AddCommGroupWithOnestatement and proof · cited by 61
- Int.castAddHomproof · cited by 17
Cited by9
Results whose statement or proof uses this declaration.
- ArithmeticFunction.intCoe_mulproof · cited by 2
- Polynomial.smeval_neg_natproof · cited by 1
- ZMod.erdos_ginzburg_zivproof · cited by 1
- Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_oneproof · cited by 1
- Int.cast_finsupp_sumproof · cited by 0
- Int.sum_modEq_iteproof · cited by 0
- Int.sum_modEq_singleproof · cited by 0
- numDerangements_tendsto_inv_eproof · cited by 0
- ArithmeticFunction.sum_moebius_mul_log_eqproof · cited by 0