src/HOL/Algebra/Multiplicative_Group.thy
changeset 68551 b680e74eb6f2
parent 68445 c183a6a69f2d
child 68561 5e85cda58af6
     1.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jun 29 23:04:36 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sat Jun 30 15:44:04 2018 +0100
     1.3 @@ -590,7 +590,11 @@
     1.4  
     1.5  lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
     1.6  
     1.7 -context field begin
     1.8 +context field 
     1.9 +begin
    1.10 +
    1.11 +lemma mult_of_is_Units: "mult_of R = units_of R" 
    1.12 +  unfolding mult_of_def units_of_def using field_Units by auto
    1.13  
    1.14  lemma field_mult_group :
    1.15    shows "group (mult_of R)"