equal
deleted
inserted
replaced
87 "x \<in> Units G ==> inv x \<in> carrier G" |
87 "x \<in> Units G ==> inv x \<in> carrier G" |
88 apply (unfold Units_def m_inv_def, auto) |
88 apply (unfold Units_def m_inv_def, auto) |
89 apply (rule theI2, fast) |
89 apply (rule theI2, fast) |
90 apply (fast intro: inv_unique, fast) |
90 apply (fast intro: inv_unique, fast) |
91 done |
91 done |
|
92 |
|
93 lemma (in monoid) Units_l_inv_ex: |
|
94 "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" |
|
95 by (unfold Units_def) auto |
|
96 |
|
97 lemma (in monoid) Units_r_inv_ex: |
|
98 "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" |
|
99 by (unfold Units_def) auto |
92 |
100 |
93 lemma (in monoid) Units_l_inv: |
101 lemma (in monoid) Units_l_inv: |
94 "x \<in> Units G ==> inv x \<otimes> x = \<one>" |
102 "x \<in> Units G ==> inv x \<otimes> x = \<one>" |
95 apply (unfold Units_def m_inv_def, auto) |
103 apply (unfold Units_def m_inv_def, auto) |
96 apply (rule theI2, fast) |
104 apply (rule theI2, fast) |
269 |
277 |
270 lemma (in group) inv_closed [intro, simp]: |
278 lemma (in group) inv_closed [intro, simp]: |
271 "x \<in> carrier G ==> inv x \<in> carrier G" |
279 "x \<in> carrier G ==> inv x \<in> carrier G" |
272 using Units_inv_closed by simp |
280 using Units_inv_closed by simp |
273 |
281 |
|
282 lemma (in group) l_inv_ex [simp]: |
|
283 "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" |
|
284 using Units_l_inv_ex by simp |
|
285 |
|
286 lemma (in group) r_inv_ex [simp]: |
|
287 "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" |
|
288 using Units_r_inv_ex by simp |
|
289 |
274 lemma (in group) l_inv [simp]: |
290 lemma (in group) l_inv [simp]: |
275 "x \<in> carrier G ==> inv x \<otimes> x = \<one>" |
291 "x \<in> carrier G ==> inv x \<otimes> x = \<one>" |
276 using Units_l_inv by simp |
292 using Units_l_inv by simp |
277 |
293 |
278 subsection {* Cancellation Laws and Basic Properties *} |
294 subsection {* Cancellation Laws and Basic Properties *} |