# HG changeset patch
# User Manuel Eberl <manuel@pruvisto.org>
# Date 1744987883 -7200
# Node ID b4d4ad6fb9bdffb321a14ef73b5d2bc50ec26000
# Parent  bb1955def6873407b20d67fc38d6fa0c11ccd2c3
removed name clash in some lemmas

diff -r bb1955def687 -r b4d4ad6fb9bd src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Apr 18 12:33:01 2025 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Apr 18 16:51:23 2025 +0200
@@ -1832,7 +1832,7 @@
     by (subst (asm) insert.IH [symmetric]) (use insert.hyps in simp)
 qed auto
 
-lemma prod_diff1:
+lemma prod_diff_conv_sum:
   fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
   assumes finite: "finite A"
   shows   "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * (\<Prod>x\<in>A-X. f1 x))"
@@ -1846,7 +1846,7 @@
   finally show ?thesis .
 qed
 
-lemma prod_diff2:
+lemma prod_diff_conv_sum':
   fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
   assumes finite: "finite A"
   shows   "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"