author Andreas Lochbihler Wed, 11 Nov 2015 09:06:30 +0100 changeset 61628 8dd2bd4fe30b parent 61626 c304402cc3df child 61629 90f54d9e63f2
 src/HOL/Algebra/Coset.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Group.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Algebra/Coset.thy	Tue Nov 10 23:41:20 2015 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Nov 11 09:06:30 2015 +0100
@@ -759,6 +759,9 @@
order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
where "order S = card (carrier S)"

+lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
+by(auto simp add: order_def card_gt_0_iff)
+
lemma (in group) rcosets_part_G:
assumes "subgroup H G"
shows "\<Union>(rcosets H) = carrier G"```
```--- a/src/HOL/Algebra/Group.thy	Tue Nov 10 23:41:20 2015 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Nov 11 09:06:30 2015 +0100
@@ -44,6 +44,9 @@
in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
end

+lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
+by(simp add: int_pow_def nat_pow_def)
+
locale monoid =
fixes G (structure)
assumes m_closed [intro, simp]:
@@ -187,6 +190,9 @@
with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
qed

+lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
+by auto
+
text \<open>Power\<close>

lemma (in monoid) nat_pow_closed [intro, simp]:
@@ -434,7 +440,16 @@
by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
qed

-
+lemma (in group) int_pow_diff:
+  "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
+by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
+
+lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"