src/HOL/Algebra/Divisibility.thy
changeset 68399 0b71d08528f0
parent 68004 a8a20be7053a
child 68470 7ddcce75c3ee
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -50,14 +50,6 @@
     1.4  
     1.5  subsection \<open>Products of Units in Monoids\<close>
     1.6  
     1.7 -lemma (in monoid) Units_m_closed[simp, intro]:
     1.8 -  assumes h1unit: "h1 \<in> Units G"
     1.9 -    and h2unit: "h2 \<in> Units G"
    1.10 -  shows "h1 \<otimes> h2 \<in> Units G"
    1.11 -  unfolding Units_def
    1.12 -  using assms
    1.13 -  by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)
    1.14 -
    1.15  lemma (in monoid) prod_unit_l:
    1.16    assumes abunit[simp]: "a \<otimes> b \<in> Units G"
    1.17      and aunit[simp]: "a \<in> Units G"