Theorems · Theorem · ring theory
Finsupp.sum_zsmul
∀ {α : Type u_1} {N : Type u_16} [inst : SubtractionCommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℤ) (g : α → N),
(f.sum fun a b => b • g a) = ∑ a, f a • g a- Cited by
- 4 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SubtractionCommMonoidFintype
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.
- DFunLike.coestatement · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- Finsuppstatement and proof · cited by 5,255
- Finset.sumstatement · cited by 5,195
- Finset.univstatement · cited by 3,473
- Finsupp.sumstatement · cited by 481
- SubtractionCommMonoidstatement and proof · cited by 79
- Finsupp.sum_fintypeproof · cited by 32
- zero_zsmulproof · cited by 19
Cited by4
Results whose statement or proof uses this declaration.
- ZLattice.exists_finsetSum_norm_rpow_le_tsumproof · cited by 2
- AddSubgroup.mem_closure_range_iff_of_fintypeproof · cited by 1
- PeriodPair.latticeEquiv_symm_applyproof · cited by 0
- AddSubgroup.exists_of_mem_closure_rangeproof · cited by 0