equal
deleted
inserted
replaced
1436 lemma (in monoid) units_of_inv: |
1436 lemma (in monoid) units_of_inv: |
1437 assumes "x \<in> Units G" |
1437 assumes "x \<in> Units G" |
1438 shows "m_inv (units_of G) x = m_inv G x" |
1438 shows "m_inv (units_of G) x = m_inv G x" |
1439 by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one) |
1439 by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one) |
1440 |
1440 |
|
1441 lemma units_of_units [simp] : "Units (units_of G) = Units G" |
|
1442 unfolding units_of_def Units_def by force |
|
1443 |
1441 lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G" |
1444 lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G" |
1442 apply (auto simp add: image_def) |
1445 apply (auto simp add: image_def) |
1443 by (metis inv_closed inv_solve_left m_closed) |
1446 by (metis inv_closed inv_solve_left m_closed) |
1444 |
1447 |
1445 lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G" |
1448 lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G" |