--- a/src/HOL/Algebra/Group.thy Wed Apr 03 12:55:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy Wed Apr 03 14:55:30 2019 +0100
@@ -9,6 +9,11 @@
imports Complete_Lattice "HOL-Library.FuncSet"
begin
+(*MOVE*)
+lemma image_paired_Times:
+ "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+ by auto
+
section \<open>Monoids and Groups\<close>
subsection \<open>Definitions\<close>
@@ -1250,10 +1255,6 @@
using assms
by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)
-lemma image_paired_Times:
- "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
- by auto
-
lemma iso_paired2:
assumes "group G" "group H"
shows "(\<lambda>(x,y). (f x,g y)) \<in> iso (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> iso G G' \<and> g \<in> iso H H'"