src/HOL/GroupTheory/Sylow.thy
changeset 11468 02cd5d5bc497
parent 11443 77ed7e2b56c8
child 13583 5fcc8bf538ee
     1.1 --- a/src/HOL/GroupTheory/Sylow.thy	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/GroupTheory/Sylow.thy	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4      M1 :: "'a set"
     1.5    assumes
     1.6      M_in_quot "M \\<in> calM // RelM"
     1.7 -    not_dvd_M "~(p ^ (exponent p m + 1) dvd card(M))"
     1.8 +    not_dvd_M "~(p ^ Suc(exponent p m) dvd card(M))"
     1.9      M1_in_M   "M1 \\<in> M"
    1.10    defines
    1.11     H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"