equal
deleted
inserted
replaced
643 lemma (in monoid) Units_pow_closed : |
643 lemma (in monoid) Units_pow_closed : |
644 fixes d :: nat |
644 fixes d :: nat |
645 assumes "x \<in> Units G" |
645 assumes "x \<in> Units G" |
646 shows "x [^] d \<in> Units G" |
646 shows "x [^] d \<in> Units G" |
647 by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow) |
647 by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow) |
648 |
|
649 lemma (in comm_monoid) is_monoid: |
|
650 shows "monoid G" by unfold_locales |
|
651 |
|
652 declare comm_monoid.is_monoid[intro?] |
|
653 |
648 |
654 lemma (in ring) r_right_minus_eq[simp]: |
649 lemma (in ring) r_right_minus_eq[simp]: |
655 assumes "a \<in> carrier R" "b \<in> carrier R" |
650 assumes "a \<in> carrier R" "b \<in> carrier R" |
656 shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b" |
651 shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b" |
657 using assms by (metis a_minus_def add.inv_closed minus_equality r_neg) |
652 using assms by (metis a_minus_def add.inv_closed minus_equality r_neg) |