# HG changeset patch
# User nipkow
# Date 1604404638 -3600
# Node ID 55a50f65c928f4246f4a7a0db1b8d3fa98aa2c97
# Parent  15aa84226a5766779bfd29065c71881a2aca2cf2
added lemma

diff -r 15aa84226a57 -r 55a50f65c928 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Nov 03 11:09:22 2020 +0100
+++ b/src/HOL/Groups_List.thy	Tue Nov 03 12:57:18 2020 +0100
@@ -301,6 +301,10 @@
   finally show ?thesis by(simp add:sum_list_map_eq_sum_count)
 qed
 
+lemma sum_list_replicate: "sum_list (replicate n c) = of_nat n * c"
+by(induction n)(auto simp add: distrib_right)
+
+
 lemma sum_list_nonneg:
     "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
   by (induction xs) simp_all