Theorems · Theorem · group theory
Multiset.sum_replicate
∀ {M : Type u_3} [inst : AddCommMonoid M] (n : ℕ) (a : M), (Multiset.replicate n a).sum = n • a- Cited by
- 30 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- Multiset.sumstatement · cited by 388
- Multiset.replicatestatement · cited by 88
- List.sum_replicateproof · cited by 19
Cited by30
Results whose statement or proof uses this declaration.
- Finset.sum_constproof · cited by 254
- Finset.sum_const_zeroproof · cited by 219
- Polynomial.natDegree_multiset_prod_X_sub_C_eq_cardproof · cited by 6
- Polynomial.natDegree_multiset_prod_of_monicproof · cited by 4
- Multiset.toFinset_sum_count_eqproof · cited by 3
- Multiset.card_productproof · cited by 3
- Multiset.bind_zeroproof · cited by 3
- Int.ModEq.multisetSum_map_zeroproof · cited by 2
- Nat.uniformBell_mul_eqproof · cited by 2
- Multiset.sum_map_zeroproof · cited by 1
- Equiv.Perm.sign_of_cycleType_eq_replicateproof · cited by 1
- Equiv.Perm.isCycle_of_prime_orderproof · cited by 1