# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1513840999 -3600
# Node ID ab10ea1d6fd064bf0c7960778ae7e80a0310a8b6
# Parent  43ed806acb95226cb25dea2981a13b278a0ad0d5
Some lemmas on complex numbers and coprimality

diff -r 43ed806acb95 -r ab10ea1d6fd0 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Dec 20 22:07:05 2017 +0100
+++ b/src/HOL/Complex.thy	Thu Dec 21 08:23:19 2017 +0100
@@ -204,6 +204,18 @@
 lemma complex_Im_fact [simp]: "Im (fact n) = 0"
   by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
 
+lemma Re_prod_Reals: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<real>) \<Longrightarrow> Re (prod f A) = prod (\<lambda>x. Re (f x)) A"
+proof (induction A rule: infinite_finite_induct)
+  case (insert x A)
+  hence "Re (prod f (insert x A)) = Re (f x) * Re (prod f A) - Im (f x) * Im (prod f A)"
+    by simp
+  also from insert.prems have "f x \<in> \<real>" by simp
+  hence "Im (f x) = 0" by (auto elim!: Reals_cases)
+  also have "Re (prod f A) = (\<Prod>x\<in>A. Re (f x))" 
+    by (intro insert.IH insert.prems) auto
+  finally show ?case using insert.hyps by simp
+qed auto
+
 
 subsection \<open>The Complex Number $i$\<close>
 
@@ -512,6 +524,9 @@
 lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \<longleftrightarrow> z = 0"
   by (simp add: complex_eq_iff)
 
+lemma complex_cnj_one_iff [simp]: "cnj z = 1 \<longleftrightarrow> z = 1"
+  by (simp add: complex_eq_iff)
+
 lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
   by (simp add: complex_eq_iff)
 
diff -r 43ed806acb95 -r ab10ea1d6fd0 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Dec 20 22:07:05 2017 +0100
+++ b/src/HOL/Rings.thy	Thu Dec 21 08:23:19 2017 +0100
@@ -1263,6 +1263,16 @@
   "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
   using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
 
+lemma coprime_absorb_left:
+  assumes "x dvd y"
+  shows   "coprime x y \<longleftrightarrow> is_unit x"
+  using assms coprime_common_divisor is_unit_left_imp_coprime by auto
+
+lemma coprime_absorb_right:
+  assumes "y dvd x"
+  shows   "coprime x y \<longleftrightarrow> is_unit y"
+  using assms coprime_common_divisor is_unit_right_imp_coprime by auto
+
 end
 
 class unit_factor =