Theorems · Theorem · group theory
List.sum_replicate
∀ {M : Type u_2} [inst : AddMonoid M] (n : ℕ) (a : M), (List.replicate n a).sum = n • a- Cited by
- 19 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- zero_nsmulproof · cited by 137
- succ_nsmul'proof · cited by 25
Cited by19
Results whose statement or proof uses this declaration.
- Multiset.sum_replicateproof · cited by 30
- List.sum_le_card_nsmulproof · cited by 3
- List.sum_eq_card_nsmulproof · cited by 2
- List.sum_eq_zero_iffproof · cited by 2
- Composition.eq_ones_iffproof · cited by 1
- List.sum_toFinset_count_eq_lengthproof · cited by 1
- Set.mem_nsmulproof · cited by 1
- Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digitsproof · cited by 1
- AddMonoidAlgebra.sup_support_pow_leproof · cited by 1
- Int.ModEq.listSum_map_zeroproof · cited by 1
- Composition.ones_sizeUpToproof · cited by 1
- Finset.small_nsmul_of_small_triplingproof · cited by 1