src/HOL/Algebra/Group.thy
changeset 68551 b680e74eb6f2
parent 68517 6b5f15387353
child 68555 22d51874f37d
     1.1 --- a/src/HOL/Algebra/Group.thy	Fri Jun 29 23:04:36 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat Jun 30 15:44:04 2018 +0100
     1.3 @@ -1438,6 +1438,9 @@
     1.4    shows "m_inv (units_of G) x = m_inv G x"
     1.5    by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
     1.6  
     1.7 +lemma units_of_units [simp] : "Units (units_of G) = Units G"
     1.8 +  unfolding units_of_def Units_def by force
     1.9 +
    1.10  lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
    1.11    apply (auto simp add: image_def)
    1.12    by (metis inv_closed inv_solve_left m_closed)