src/HOL/Algebra/AbelCoset.thy
changeset 35849 b5522b51cb1e
parent 35848 5443079512ea
child 39910 10097e0a9dbd
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 16:51:37 2010 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 17:12:31 2010 +0100
     1.3 @@ -1,13 +1,11 @@
     1.4 -(*
     1.5 -  Title:     HOL/Algebra/AbelCoset.thy
     1.6 -  Author:    Stephan Hohe, TU Muenchen
     1.7 +(*  Title:      HOL/Algebra/AbelCoset.thy
     1.8 +    Author:     Stephan Hohe, TU Muenchen
     1.9  *)
    1.10  
    1.11  theory AbelCoset
    1.12  imports Coset Ring
    1.13  begin
    1.14  
    1.15 -
    1.16  subsection {* More Lifting from Groups to Abelian Groups *}
    1.17  
    1.18  subsubsection {* Definitions *}
    1.19 @@ -520,6 +518,7 @@
    1.20  text {* The isomorphism theorems have been omitted from lifting, at
    1.21    least for now *}
    1.22  
    1.23 +
    1.24  subsubsection{*The First Isomorphism Theorem*}
    1.25  
    1.26  text{*The quotient by the kernel of a homomorphism is isomorphic to the 
    1.27 @@ -642,6 +641,7 @@
    1.28  by (rule group_hom.FactGroup_iso[OF a_group_hom,
    1.29      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    1.30  
    1.31 +
    1.32  subsubsection {* Cosets *}
    1.33  
    1.34  text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
    1.35 @@ -726,7 +726,6 @@
    1.36      folded A_RCOSETS_def, simplified monoid_record_simps])
    1.37  
    1.38  
    1.39 -
    1.40  subsubsection {* Addition of Subgroups *}
    1.41  
    1.42  lemma (in abelian_monoid) set_add_closed: