Theorems · Theorem · sequences and series
SummationFilter.symmetricIcc_eq_map_Icc_nat
(SummationFilter.symmetricIcc ℤ).filter = Filter.map (fun N => Finset.Icc (-↑N) ↑N) Filter.atTop
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Filterstatement · cited by 8,121
- Filter.atTopstatement and proof · cited by 2,405
- Filter.mapstatement and proof · cited by 819
- Finset.Iccstatement and proof · cited by 348
- SummationFilter.filterstatement · cited by 110
- Filter.map_mapproof · cited by 80
- SummationFilter.symmetricIccstatement · cited by 16
- SummationFilter.symmetricIcc_filterproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- HasSum.hasSum_symmetricIco_of_hasSum_symmetricIccproof · cited by 3
- EisensteinSeries.hasSum_e2Summand_symmetricIccproof · cited by 3
- HasProd.hasProd_symmetricIco_of_hasProd_symmetricIccproof · cited by 2