SSL sylow_theorems.prf
Interaktion und
(sylow_theoremsnil 3531235292"" (rewrite "T_is_group" ) nil nil )nil sylow_theorems nil )) nil ))nil 3531141392"" (skosimp*)"" (typepred "P!1" "G!1" )"" (hide -1)"" (lemma "finite_subgroups" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil group "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )set type-eq-decl nil sets nil )nil sylow_theorems nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil group "algebra/" ))nil ))nil 3531141392"" (skosimp*)"" (hide -1)"" (typepred "H!1" "G!1" )"" (hide -1)"" (lemma "finite_subgroups" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil group "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil group "algebra/" ))nil ))nil 3530954477"" (skosimp)"" (inst 1 "one" )"1" (rewrite "left_coset_one[T,*,one]" ) nil nil )"2" (typepred "G!1" )"2" (expand * "group?" "monoid?" "monad?" "member" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"group[T, *, one]" sylow_theorems nil )nil group "algebra/" )"bool" group_def "algebra/" )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sylow_theorems nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil cosets "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil )"bool" monad_def "algebra/" )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3530954477"" (skosimp*)"" (rewrite "left_cosets_group[T, *, one]" ) nil nil )) nil )nil factor_groups "algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )nil group "algebra/" )"boolean" normal_subgroups "algebra/" )nil normal_subgroups "algebra/" )nil sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil ))nil ))nil 3530954477"" (skosimp*)"" (typepred "N!1" )"" (hide -1)"" (lemma "normal_subgroup_tran[T, *, one]" )"1" (inst -1 "G!1" "H!1" "N!1" ) (("1" (assert ) nil nil ))nil )"2" (hide (-1 -2 2)) (("2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )set type-eq-decl nil sets nil )nil sylow_theorems nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil groups_scaf nil )"set" sets nil )nil group "algebra/" )"bool" group_def "algebra/" )nil sylow_theorems nil ))nil ))nil 3530981159"" (skosimp*)"" (prop)"1" (hide (-2 -3))"1" (skosimp)"1" (inst?)"1" (hide -1)"1" (typepred "a!1" "H!1" )"1" (expand * "subgroup?" "subset?" "member" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "/" )"2" (expand "restrict" )"2" (expand "left_cosets" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"group[T, *, one]" sylow_theorems nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"(H!1)" sylow_theorems nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sylow_theorems nil )"group[left_cosets(G, N), mult(G, N), N]" nil )"setofsets[T]" right_left_cosets nil )"R" restrict nil ))nil ))nil 3530954523"" (skosimp*)"" (lemma "natural_homo[T, *, one,T, *, one]" )"1" (inst -1 "G!1" "N!1" )"1" (skosimp)"1" "correspondence_theorem[T,*,one,left_cosets(G!1,N!1),mult(G!1,N!1),N!1]" )"1" (inst?)"1" (assert )"1" (skosimp)"1" (expand "bijective?" )"1" (flatten)"1" (hide -7)"1" (expand "surjective?" )"1" (inst -3 "S!1" )"1" (skosimp)"1" "x!1" )"1" "1" "x!1" )"1" "1" replace -3 -2 rl)"1" "1" expand "subgroup?" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace -1 1 rl)"2" "2" "1" "1" "1" expand "extend" )"1" "1" "1" expand "image" )"1" "1" "1" "x!3" )"1" expand "/" )"1" expand *"restrict" "left_cosets" )"1" "1" assert )nil nil )"2" "x!3" )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "image" )"1" "1" expand *"/" "restrict" "left_cosets" )"1" "1" "a!1" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "a!1" "x!1" )"2" "2" expand *"subgroup?" "subset?" "member" )"2" "2" expand "restrict" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"/" "restrict" "left_cosets" )"2" "2" "a!1" "x!1" )"2" "2" expand *"subgroup?" "subset?" "member" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "T_is_group" )nil nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T_is_group" ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (rewrite "left_cosets_group[T, *, one]" ) nil nil ))nil )"3" (hide-all-but 1)"3" (inst 1 "one" )"1" (rewrite "left_coset_one[T, *, one]" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )nil sylow_theorems nil )nil homomorphism_lemmas nil )"set" sets nil )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )nil cosets "algebra/" )nil factor_groups "algebra/" )"group[left_cosets(G, N), mult(G, N), N]" nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )"(x!1)" sylow_theorems nil )"(x!1)" sylow_theorems nil )"bool" sets nil )"setofsets[T]" right_left_cosets nil )"(restrict[T, (G!1), bool](x!1))" nil )"bool" booleans nil )"R" extend nil )"set[R]" function_image nil )"R" restrict nil )"group[T, *, one]" sylow_theorems nil )"normal_subgroup[T, *, one](G!1)" nil )"[(G!1) -> (G!1 / N!1)]" sylow_theoremsnil )"[bool, bool -> bool]" booleans nil )"subgroup_contain[T, *, one](G!1, kernel(G!1, G!1 / N!1)(pi!1))" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )nil groups_scaf nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" functions nil )nil isomorphism_theorems nil )"[T, T -> boolean]" equalities nil )"set[T]" cosets "algebra/" )nil cosets "algebra/" )"left_cosets(G, H)" factor_groups "algebra/" )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil group "algebra/" ))nil 3531043400 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3531043400 ("" (subtype-tcc) nil nil )"posnat" monad "algebra/" )"real" exponentiation nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" )"posnat" exponentiation nil ))nil ))nil 3531043400"" (skosimp*)"" (hide -)"" (typepred "G!1" "H!1" )"" (lemma "finite_subgroups[T, *, one]" )"" (inst?)"" (assert )"" (hide (-2 -4))"" (expand * "group?" "finite_group?" "finite_monad?" )"" (expand "monoid?" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" ))nil ))nil 3531043400 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" )"posnat" monad "algebra/" )"real" exponentiation nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"posnat" exponentiation nil ))nil ))nil 3531043400"" (skosimp*)"" (hide -) (("" (typepred "i!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil ))nil ))nil 3531043400"" (skosimp*)"" (hide -)"" (typepred "G!1" "K!1" )"" (lemma "finite_subgroups[T, *, one]" )"" (inst?)"" (assert )"" (hide (-2 -4))"" (expand * "group?" "finite_group?" "finite_monad?" )"" (expand "monoid?" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" ))nil ))nil 3531043866"" (induct "i" )"1" (hide 2)"1" (typepred "i!1" ) (("1" (propax) nil nil )) nil )) nil )"2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1 = 0" :hide? T)"1" (hide (-1 -2 -5 -6))"1" (lemma "cauchy_cor[T,*,one]" )"1" (inst -1 "G!1" "p!1" )"1" (prop)"1" (rewrite "expt_x1" ) nil nil )"2" (skosimp*)"2" (assert )"2" (rewrite "expt_x1" )"2" (rewrite "expt_x0" )"2" (inst 1 "H!1" )"2" (assert )"2" (lemma "one_is_subgroup" )"2" "H!1" )"2" "order_is_1" )"2" "2" assert )"2" expand "one_group" )"2" replace -1 -2 rl)"2" expand "normal_subgroup?" )"2" assert )"2" "2" expand *"subset?" "member" )"2" "2" expand "*" )"2" "2" "h!1" )"2" "2" "h!2" )"2" "2" expand "singleton" )"2" "2" "2" rewrite "one_right" )"2" rewrite "inv_left" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 1)"3" (lemma "divides_power" )"3" (inst?)"3" (replaces -3)"3" (hide -2)"3" (rewrite "divides_prod1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 1)"4" (lemma "divides_power" )"4" (inst?)"4" (replaces -3)"4" (hide -2)"4" (rewrite "divides_prod1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (- 2)) (("2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (prop)"1" (inst -1 "m!1" "n!1" "p!1" "G!1" )"1" (assert )"1" (flatten)"1" (hide -2)"1" (skosimp)"1" (lemma "normalizer_index[T,*,one]" )"1" (inst -1 "p!1" "G!1" "H!1" )"1" (prop)"1" (lemma "card_factor[T,*,one]" )"1" "1" "1" rewrite "card_extend[set[T], left_cosets[T, *, one](normalizer(G!1, H!1), H!1)]" )"1" replace -1 -2 rl)"1" "1" "cauchy_cor[left_cosets(normalizer(G!1, H!1),H!1),mult(normalizer(G!1, H!1),H!1),H!1]" )"1" "normalizer(G!1, H!1) / H!1" "p!1" )"1" "1" "1" "subgroup_is_factor" )"1" "normalizer(G!1, H!1)" "H!1" "H!2" )"1" "1" "1" "1" "Lagrange_index[T,*,one]" )"1" "H!3" "H!1" )"1" assert )"1" "card_factor[T,*,one]" )"1" "H!3" "H!1" )"1" "1" rewrite "card_extend[set[T], left_cosets[T, *, one](H!3, H!1)]" )"1" replace "1" "1" replace "1" "card(H!3 / H!1) = p!1" "1" "H!3" )"1" "1" rewrite "expt_plus" )"1" rewrite "expt_x1" )nil nil ))nil ))nil )"2" "2" "H!3" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_transitive[T, *, one]" )"2" "G!1" "normalizer(G!1, H!1)" "H!3" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "order" )"2" rewrite "card_def[left_cosets(normalizer(G!1, H!1), H!1)]" )"2" rewrite "card_def[left_cosets[T, *, one](H!3, H!1)]" )"2" replace "2" "2" expand "Card" )"2" expand "inj_set" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" "restrict_finite[setof[T], left_cosets[T, *, one](H!3, H!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "H!3" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )"1" "finite_subgroups" )"1" "H!3" "normalizer(G!1, H!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "H!3" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )"1" "finite_subgroups" )"1" "H!3" "normalizer(G!1, H!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "H!3" "H!1" )"3" "3" "normal_in_normalizer[T, *, one]" )"3" "3" assert )"3" "normal_subgroup_tran[T, *, one]" )"3" "normalizer(G!1, H!1)" "H!3" "H!1" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "H!1" "G!1" )"2" "2" "finite_subgroups" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "H!3" )"3" "3" "normalizer_is_subgroup[T, *, one]" )"3" "3" assert )"3" "G!1" )"3" "finite_subgroups" )"3" "1" assert )"1" "finite_subgroups" )"1" "H!3" "normalizer(G!1, H!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "order" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" expand "finite_group?" )"2" "1" "divide_TCC5[T, *, one]" )"1" "1" "1" "normal_in_normalizer[T, *, one]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil )"2" "restrict_finite[setof[T],left_cosets[T, *, one](normalizer[T, *, one](G!1, H!1), H!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil )"2" "2" "left_cosets_group[T, *, one]" )"2" "1" "1" "normal_in_normalizer[T, *, one]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_is_group[T, *, one]" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"3" "3" "one" )"1" rewrite "left_coset_one" )nil nil )"2" expand "normalizer" )"2" expand "extend" )"2" "1" rewrite "inv_one" )"1" rewrite "left_coset_one" )"1" rewrite "right_coset_one" )nil nil ))nil ))nil )"2" rewrite "one_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" "restrict_finite[setof[T],left_cosets[T, *, one](normalizer[T, *, one](G!1, H!1), H!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" (assert ) nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "normal_in_normalizer[T, *, one]" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_is_group[T, *, one]" )"2" "1" (assert ) nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil )"2" "2" (rewrite "T_is_group" ) nil nil ))nil ))nil )"2" (hide-all-but (-1 -3 1))"2" "p_group_iff_power[T, *, one]" )"2" "2" assert )"2" (inst?) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 -4 -6 1))"3" "Lagrange_index[T,*,one]" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "div_cancel4" )"1" "p!1 ^ j!1" "index(G!1, H!1)" "p!1 ^ n!1 * m!1" )"1" "1" "1" rewrite "times_div2" "1" rewrite "exponentiation.expt_div" )"1" "expt_plus" )"1" "1" "n!1 - j!1 - 1" "p!1" )"1" assert )"1" rewrite "expt_x1" )"1" "1" "p!1 ^ (-1 - j!1 + n!1) * m!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "H!1" )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (skosimp)"2" (lemma "normalizer_index[T,*,one]" )"2" (inst -1 "p!1" "G!1" "S!1" )"2" (prop)"1" (lemma "card_factor[T,*,one]" )"1" (inst?)"1" (prop)"1" rewrite "card_extend[set[T], left_cosets[T, *, one](normalizer(G!1, S!1), S!1)]" )"1" replace -1 -2 rl)"1" "1" "cauchy_cor[left_cosets(normalizer(G!1, S!1),S!1),mult(normalizer(G!1, S!1),S!1),S!1]" )"1" "normalizer(G!1, S!1) / S!1" "p!1" )"1" "1" "1" "subgroup_is_factor" )"1" "normalizer(G!1, S!1)" "S!1" "H!1" )"1" "1" "1" "1" "Lagrange_index[T,*,one]" )"1" "H!2" "S!1" )"1" assert )"1" "card_factor[T,*,one]" )"1" "H!2" "S!1" )"1" "1" rewrite "card_extend[set[T], left_cosets[T, *, one](H!2, S!1)]" )"1" replace "1" "1" replace "1" "card(H!2 / S!1) = p!1" "1" "H!2" )"1" "1" rewrite "expt_plus" )"1" rewrite "expt_x1" )"1" assert )"1" "1" "H!2" )"1" "1" "normal_in_normalizer[T,*,one]" )"1" "1" assert )"1" "normal_subgroup_tran[T, *, one]" )"1" "normalizer(G!1, S!1)" "H!2" "S!1" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "H!2" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_transitive[T, *, one]" )"2" "G!1" "normalizer(G!1, S!1)" "H!2" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "order" )"2" rewrite "card_def[left_cosets(normalizer(G!1, S!1), S!1)]" )"2" rewrite "card_def[left_cosets[T, *, one](H!2, S!1)]" )"2" replace "2" "2" expand "Card" )"2" expand "inj_set" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" "restrict_finite[setof[T], left_cosets[T, *, one](H!2, S!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "H!2" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )"1" "finite_subgroups" )"1" "H!2" "normalizer(G!1, S!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "H!2" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )"1" "finite_subgroups" )"1" "H!2" "normalizer(G!1, S!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "H!2" "S!1" )"3" "3" "normal_in_normalizer[T, *, one]" )"3" "3" assert )"3" "normal_subgroup_tran[T, *, one]" )"3" "normalizer(G!1, S!1)" "H!2" "S!1" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "S!1" "G!1" )"2" "2" "finite_subgroups" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "H!2" )"3" "3" "normalizer_is_subgroup[T, *, one]" )"3" "3" assert )"3" "G!1" )"3" "finite_subgroups" )"3" "1" assert )"1" "finite_subgroups" )"1" "H!2" "normalizer(G!1, S!1)" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "order" )"2" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" expand "finite_group?" )"2" "1" "divide_TCC5[T, *, one]" )"1" "1" "1" "normal_in_normalizer[T, *, one]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil )"2" "restrict_finite[setof[T],left_cosets[T, *, one](normalizer[T, *, one](G!1, S!1), S!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil )"2" "2" "left_cosets_group[T, *, one]" )"2" "1" "1" "normal_in_normalizer[T, *, one]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_is_group[T, *, one]" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"3" "3" "one" )"1" rewrite "left_coset_one" )nil nil )"2" expand "normalizer" )"2" expand "extend" )"2" "1" rewrite "inv_one" )"1" rewrite "left_coset_one" )"1" rewrite "right_coset_one" )nil nil ))nil ))nil )"2" rewrite "one_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" "restrict_finite[setof[T],left_cosets[T, *, one](normalizer[T, *, one](G!1, S!1), S!1)]" )"2" "1" assert )"1" "1" "left_cosets_partition[T,*,one]" )"1" "1" expand "finite_partition?" )"1" nil nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "G!1" )"2" "finite_subgroups" )"2" "1" (assert ) nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" "normal_in_normalizer[T, *, one]" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "subgroup_is_group[T, *, one]" )"2" "1" (assert ) nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (rewrite "T_is_group" ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T_is_group" ) nil nil )) nil ))nil )"2" (hide-all-but (-1 -3 1))"2" (lemma "p_group_iff_power[T, *, one]" )"2" (inst?)"2" (assert ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 -4 -6 1))"3" (lemma "Lagrange_index[T,*,one]" )"1" (inst?)"1" (assert )"1" "1" "1" expand "divides" )"1" "div_cancel4" )"1" "p!1 ^ j!1" "index(G!1, S!1)" "p!1 ^ n!1 * m!1" )"1" "1" "1" rewrite "times_div2" "1" rewrite "exponentiation.expt_div" )"1" "expt_plus" )"1" "1" "n!1 - j!1 - 1" "p!1" )"1" assert )"1" rewrite "expt_x1" )"1" "1" "p!1 ^ (-1 - j!1 + n!1) * m!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "S!1" )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (hide-all-but 1)"4" (typepred "K!1" )"4" (typepred "G!1" )"4" (lemma "finite_subgroups" )"4" (inst?)"4" (assert )"4" expand * "group?" "monoid?" "finite_monad?" "finite_group?" )"4" (flatten) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 2)"5" (skosimp*)"5" (hide-all-but 1)"5" (typepred "S!1" )"5" (typepred "G!1" )"5" (lemma "finite_subgroups" )"5" (inst?)"5" (assert )"5" expand * "group?" "monoid?" "finite_monad?" "finite_group?" )"5" (flatten) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide 2)"6" (skosimp*)"6" (typepred "H!1" )"6" (typepred "G!1" )"6" (lemma "finite_subgroups" )"6" (inst?)"6" (assert )"6" expand * "group?" "monoid?" "finite_monad?" "finite_group?" )"6" (flatten) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" monoid_def "algebra/" )"(total_order?[real])" nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"subgroup[T, *, one](normalizer(G!1, S!1))" nil )"nat" right_left_cosets nil )nil reals nil )nil exponentiation nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(total_order?[real])" nil )"posnat" sylow_theorems nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" sylow_theorems nil )"posnat" sylow_theorems nil )"posnat" sylow_theorems nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"posnat" exponentiation nil )"int" integers nil )"posrat" nil )"posrat" nil )nil real_props nil )nil real_props nil )nil p_groups nil )nil right_left_cosets nil )nil right_left_cosets nil )nil sylow_theorems nil )"subgroup[T, *, one](normalizer(G!1, H!1))" nil )nil restrict_set_props nil )nil defined_types nil )nil right_left_cosets nil )nil group "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )"setofsets[T]" right_left_cosets nil )nil finite_sets nil )"(nonempty?[nat])" finite_sets nil )nil reals nil )nil exponentiation nil )nil normalizer_centralizernil )nil groups_scaf nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nonneg_int" nil )nil normalizer_centralizer nil )nil groups_scaf nil )nil lagrange_index nil )nil factor_groups "algebra/" )nil group "algebra/" )nil cosets "algebra/" )"R" extend nil )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )nil group "algebra/" )nil cosets "algebra/" )nil extend_set_props nil )"bool" finite_sets nil )nil finite_sets nil )nil normal_subgroups "algebra/" )"left_cosets(G, H)" factor_groups "algebra/" )"group[left_cosets(G, N), mult(G, N), N]" nil )nil cosets "algebra/" )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"finite_group[T, *, one]" sylow_theoremsnil )"{S: set[T] | subset?(S, G)}" nil )nil p_groups nil )"posint" nil )nil sylow_theorems nil )nil divides nil )nil general_properties nil )nil group "algebra/" )nil monad "algebra/" )"non_empty_finite_set[T]" countable_props "sets_aux/" )"bool" sets nil )"bool" sets nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )"{y | x * y = one AND y * x = one}" group"algebra/" )"(singleton?)" sets nil )nil group "algebra/" )nil group "algebra/" )"finite_group" group "algebra/" )nil exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"set" sets nil )nil cauchy nil )"posint" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"boolean" normal_subgroups "algebra/" )nil defined_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil integers nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" primes "ints/" )"[T, T -> boolean]" equalities nil )"bool" monad_def "algebra/" )nil monad "algebra/" )"posnat" monad "algebra/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"bool" reals nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"int" integers nil )"posint" exponentiation nil ))nil 3531303927 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3531303927 ("" (subtype-tcc) nil nil )"posnat" monad "algebra/" )"real" exponentiation nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"boolean" notequal nil )"bool" primes "ints/" )"posnat" exponentiation nil ))nil ))nil 3531304355"" (skosimp*)"" (hide -)"" (typepred "G!1" "K!1" )"" (lemma "finite_subgroups[T, *, one]" )"" (inst?)"" (assert )"" (hide (-2 -4))"" (expand * "group?" "finite_group?" "finite_monad?" )"" (expand "monoid?" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" ))nil ))nil 3531303962"" (induct "i" )"1" (hide 2)"1" (typepred "i!1" ) (("1" (propax) nil nil )) nil )) nil )"2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1 = 0" :hide? T)"1" (hide (-1 -2 -5))"1" (assert )"1" (lemma "First_Sylow_Theorem" )"1" (inst?)"1" (inst -1 "n!1" )"1" (assert )"1" (flatten)"1" (hide -1)"1" (inst -1 "H!1" )"1" (assert )"1" (skosimp)"1" "1" expand "normal_subgroup?" )"1" "1" "1" "K!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "First_Sylow_Theorem" )"2" (inst?)"2" (inst -1 "n!1 - j!1" )"2" (assert )"2" (flatten)"2" (hide -1)"2" (inst -1 "H!1" )"2" (assert )"2" (skosimp)"2" "m!1" "n!1" "p!1" "G!1" "K!1" )"2" assert )"2" "2" "2" expand "normal_subgroup?" )"2" "2" "2" "K!2" )"2" "subgroup_transitive[T,*,one]" )"1" "K!2" "K!1" "H!1" )"1" assert )nil nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (lemma "p_group_is_subgroup_TCC3" )"4" (inst -1 "i!2" "m!1" "n!1" "p!1" "G!1" "H!1" )"4" (assert ) (("4" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"5" (hide 2)"5" (skosimp*)"5" (lemma "First_Sylow_Theorem_TCC3" )"5" (inst -1 "i!2" "m!1" "n!1" "p!1" "G!1" )"5" (assert ) (("5" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil sylow_theorems nil )"nat" sylow_theorems nil )nil sylow_theorems nil )"nat" sylow_theorems nil )"int" integers nil )"posint" nil )nil groups_scaf nil )"set" sets nil )nil sylow_theorems nil )"(total_order?[real])" nil )nil sylow_theorems nil )"boolean" normal_subgroups "algebra/" )"(total_order?[real])" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"odd_int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )nil defined_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil integers nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" monad_def "algebra/" )nil monad "algebra/" )"posnat" monad "algebra/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"bool" reals nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"bool" primes "ints/" )"int" integers nil )"posint" exponentiation nil ))nil 3531210392"" (skosimp*)"" (hide -)"" (typepred "G!1" "P!1" )"" (lemma "finite_subgroups[T, *, one]" )"" (inst?)"" (assert )"" (hide (-2 -4))"" (expand * "group?" "finite_group?" "finite_monad?" )"" (expand "monoid?" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" ))nil ))nil 3531210414"" (skosimp*)"" (prop)"1" (expand "p_subgroup_sylow?" )"1" (flatten)"1" (lemma "p_group_iff_power[T, *, one]" )"1" (inst?)"1" (assert )"1" (skosimp)"1" (case "m!2 > n!1" )"1" (hide (-3 -4))"1" (lemma "gcd_1_nd" )"1" (inst -1 "m!1" "p!1" )"1" (rewrite "gcd_sym" )"1" (assert )"1" "1" "Lagrange" )"1" "G!1" "P!1" )"1" assert )"1" "1" "1" expand "divides" )"1" "1" "both_sides_div1" )"1" "p!1 ^ n!1" "p!1 ^ n!1 * m!1" "p!1 ^ m!2 * x!1" )"1" "1" "1" rewrite "times_div1" "1" rewrite "div_cancel1" )"1" rewrite "times_div2" "1" rewrite "exponentiation.expt_div" )"1" "expt_plus" )"1" "1" "m!2 - n!1 - 1" "p!1" )"1" rewrite "expt_x1" )"1" assert )"1" "1" "p!1 ^ (-1 - n!1 + m!2) * x!1" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subgroups" )"2" "P!1" "G!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "p_group_is_subgroup" )"2" "n!1 - m!2" "m!1" "n!1" "p!1" "G!1" "P!1" )"1" (assert )"1" (skosimp)"1" "p_group_iff_power[T, *, one]" )"1" "p!1" "K!1" )"1" assert )"1" "1" "1" "K!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" (inst?) nil nil ))nil ))nil ))nil )"2" "2" "finite_subgroups" )"2" "K!1" "G!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "m!2 = n!1" :hide? T)"2" (hide (- 4)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "p_subgroup_sylow?" )"2" (prop)"1" (lemma "p_group_iff_power[T, *, one]" )"1" (inst -1 "p!1" "P!1" )"1" (assert ) (("1" (inst?) nil nil )) nil )) nil ))nil )"2" (skosimp)"2" (lemma "p_group_iff_power[T, *, one]" )"2" (inst?)"2" (assert )"2" (skosimp)"2" (case "m!2 > n!1" )"1" (hide (-3 -4 -5))"1" (lemma "gcd_1_nd" )"1" (inst -1 "m!1" "p!1" )"1" (rewrite "gcd_sym" )"1" assert )"1" "1" "Lagrange" )"1" "G!1" "H!1" )"1" assert )"1" "1" "1" expand "divides" )"1" "1" "both_sides_div1" )"1" "p!1 ^ n!1" "p!1 ^ n!1 * m!1" "p!1 ^ m!2 * x!1" )"1" "1" "1" rewrite "times_div1" "1" rewrite "div_cancel1" )"1" rewrite "times_div2" "1" rewrite "exponentiation.expt_div" )"1" "expt_plus" )"1" "1" "m!2 - n!1 - 1" "p!1" )"1" rewrite "expt_x1" )"1" assert )"1" "1" "p!1 ^ (-1 - n!1 + m!2) * x!1" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subgroups" )"2" "H!1" "G!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "m!2 = n!1" :hide? T)"1" (hide-all-but (-1 -3 -4 2))"1" (lemma "orders_equal[T, *, one]" )"1" (inst -1 "H!1" "P!1" )"1" (assert ) nil nil )"2" "2" "finite_subgroups" )"2" "P!1" "G!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "finite_subgroups" )"3" "H!1" "G!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "p_group_is_subgroup" )"2" "n!1 - m!2" "m!1" "n!1" "p!1" "G!1" "H!1" )"1" (assert )"1" "1" "1" "subgroup_transitive[T,*,one]" )"1" "K!1" "H!1" "P!1" )"1" assert )"1" "orders_equal[T,*,one]" )"1" "K!1" "P!1" )"1" assert )"1" "1" "1" expand "subgroup?" )"1" "subset_antisymmetric[T]" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subgroups" )"2" "P!1" "G!1" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" "finite_subgroups" )"3" "K!1" "G!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (- 4)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil sylow_theorems nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil lagrange "algebra/" )nil group "algebra/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"boolean" notequal nil )nil real_props nil )nil reals nil )nil exponentiation nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"posnat" sylow_theorems nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" sylow_theorems nil )"nat" sylow_theorems nil )"int" sylow_theorems nil )"[numfield -> numfield]" number_fields nil )"posnat" exponentiation nil )"odd_int" integers nil )nil exponentiation nil )nil exponentiation nil )"rat" rationals nil )nil real_props nil )"posrat" nil )"posrat" nil )nil real_props nil )nil real_props nil )"bool" divides nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"finite_group[T, *, one]" sylow_theoremsnil )"(strict_total_order?[real])" real_props nil )nil gcd "ints/" )nil general_properties nil )nil naturalnumbers nil )"posint" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil p_groups nil )nil sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" sylow_theorems nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"int" sylow_theorems nil )"nat" sylow_theorems nil )nil sylow_theorems nil )nil sets_lemmas nil )"(partial_order?[set[T]])" nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"set" sets nil )nil groups_scaf nil )nil finite_groups "algebra/" ))nil 3531324060"" (skosimp*)"" (lemma "conjugate_is_subgroup[T,*,one]" )"1" (inst?)"1" (hide-all-but (-1 1))"1" (assert )"1" (lemma "subgroup_is_group[T,*,one]" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide (- 2)) (("2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )nil sylow_theorems nil )nil groups_scaf nil )"set" sets nil )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil group "algebra/" )"{y | x * y = one AND y * x = one}" group"algebra/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil sylow_theorems nil ))nil ))nil 3531345595"" (skosimp*)"" (lemma "card_eq_bij[T,T]" )"" (inst -1 "P!1" "a!1 * P!1 * inv(a!1)" )"1" (prop)"1" (hide -2)"1" (lemma "p_subgroup_sylow_order" )"1" (inst-cp -1 "m!1" "n!1" "p!1" "G!1" "P!1" )"1" "m!1" "n!1" "p!1" "G!1" "a!1 * P!1 * inv(a!1)" )"1" (expand "order" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide (- 2 3))"2" (inst 1 "LAMBDA (x: (P!1)): a!1 * x * inv(a!1)" )"1" (expand "bijective?" )"1" (prop)"1" (expand "injective?" )"1" (skosimp*)"1" (rewrite "cancel_right" )"1" (rewrite "cancel_left" ) nil nil )) nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp)"2" (typepred "y!1" )"2" (expand "*" )"2" (skosimp)"2" (typepred "h!1" )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "*" )"2" (inst?) (("2" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (hide (- 2))"2" (lemma "conjugate_is_subgroup[T, *, one]" )"1" (inst?)"1" (lemma "finite_subgroups[T, *, one]" )"1" (inst?)"1" (assert )"1" (expand "finite_group?" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil )"3" (hide (- 2))"3" (lemma "finite_subgroups[T, *, one]" )"3" (inst -1 "P!1" "G!1" )"3" (assert )"3" (expand "finite_group?" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sylow_theorems nil )nil finite_sets_card_eq "finite_sets/" )nil sylow_theorems nil )nil group "algebra/" )"set" sets nil )nil groups_scaf nil )nil sylow_theorems nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"posnat" monad "algebra/" )"posint" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil group "algebra/" )nil group "algebra/" )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"bool" functions nil )"(P!1)" sylow_theorems nil )nil finite_sets nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )"(G!1)" sylow_theorems nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group"algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"finite_group[T, *, one]" sylow_theoremsnil )nil group "algebra/" )"subgroup[T, *, one](G!1)" sylow_theoremsnil ))nil 3531346917"" (skosimp*)"" (decompose-equality -4)"" (lemma "conjugate_is_p_subgroup_sylow" )"" (inst -1 "m!1" "n!1" "p!1" "G!1" "P!1" )"" (assert )"" (inst-cp -2 "P!1" )"" (iff)"" (expand * "extend" "singleton" )"" (expand "p_subgroup_sylow" -3)"" (expand "extend" )"" (prop)"" (expand "normal_subgroup?" )"" (skosimp)"" (inst -1 "inv(a!1)" )"1" rewrite "inv_inv" )"1" "inv(a!1) * P!1 * a!1" )"1" "1" "1" expand "p_subgroup_sylow" )"1" expand "extend" )"1" "1" "1" "1" "1" "1" "1" rewrite "subset_reflexive" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "conjugate_is_subgroup[T,*,one]" )"1" "G!1" "inv(a!1)" "P!1" )"1" rewrite "inv_inv" )"1" "subgroup_is_group[T,*,one]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil )"3" "3" "conjugate_is_subgroup[T,*,one]" )"1" "G!1" "inv(a!1)" "P!1" )"1" rewrite "inv_inv" )nil nil )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (rewrite "inv_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sylow_theorems nil )nil booleans nil )nil booleans nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" primes "ints/" )nil sets nil )"setofsets[T]" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" booleans nil )"R" extend nil )"bool" sets nil )"(singleton?)" sets nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"finite_set[T]" nil )"(nonempty?[T])" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"posint" exponentiation nil )"boolean" normal_subgroups "algebra/" )"finite_group[T, *, one]" sylow_theoremsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"(G!1)" sylow_theorems nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil sets_lemmas nil )nil groups_scaf nil )"set" sets nil )nil group "algebra/" )nil group "algebra/" )nil sylow_theorems nil )nil group "algebra/" )nil sylow_theoremsnil ))nil 3531143488"" (skosimp*)"" (hide -)"" (typepred "K!1" "G!1" )"" (hide -1)"" (lemma "finite_subgroups" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil group "algebra/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil group "algebra/" ))nil ))nil 3531143488"" (skosimp*)"" (hide -)"" (lemma "conjugate_is_subgroup[T,*,one]" )"1" (inst?)"1" (lemma "subgroup_is_group[T, *, one]" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (hide 2) (("2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil )nil sylow_theorems nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group"algebra/" )nil group "algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )"set" sets nil )nil groups_scaf nil )nil sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil ))nil ))nil 3531204559"" (skosimp*)"" (lemma "p_group_iff_power[T,*,one]" )"" (inst?)"" (assert )"" (skosimp)"" (lemma "Fix_congruence[T,*,one,set[T]]" )"1" "K!1" "left_cosets(G!1,P!1)" "m!2" "p!1" "alt(G!1,K!1,P!1)" )"1" (prop)"1" case "card(Fix(K!1, left_cosets(G!1, P!1))(alt(G!1, K!1, P!1))) /= 0" )"1" (hide -2)"1" (prop)"1" (lemma "nonempty_card[set[T]]" )"1" (inst?)"1" (assert )"1" "1" expand *"nonempty?" "empty?" "member" )"1" "1" "1" expand "Fix" -1)"1" expand "extend" )"1" "1" "1" expand "left_cosets" "1" "1" "1" "Fix_iff_subset[T, *, one]" )"1" "G!1" "K!1" "P!1" "a!1" )"1" assert )"1" "1" "1" expand "subgroup?" )"1" nil nil ))nil )"2" "2" "finite_subgroups" )"2" "P!1" "G!1" )"2" "K!1" "G!1" )"2" assert )"2" expand "finite_group?" )"2" case "card(K!1) = card(P!1)" )"1" "left_coset_correspondence_inv[T, *, one]" )"1" "G!1" "P!1" "a!1" )"1" assert )"1" "bijection_finite_set2[T,T]" )"1" "1" "1" "card_eq_bij[T,T]" )"1" "P!1" "a!1 * P!1 * inv(a!1)" )"1" "1" "1" replace "1" "1" expand "is_conjugate" )"1" "1" rewrite "same_card_subset" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "p_subgroup_sylow_order" )"2" "m!1" "n!1" "p!1" "G!1" "P!1" )"2" "m!1" "n!1" "p!1" "G!1" "K!1" )"2" assert )"2" "2" expand "order" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "p_subgroup_sylow_order" )"2" (inst -1 "m!1" "n!1" "p!1" "G!1" "P!1" )"2" (assert )"2" (hide (-7 -8))"2" "Lagrange_index[T, *, one]" )"2" "G!1" "P!1" )"1" assert )"1" "1" "1" rewrite "commutative_mult" )"1" rewrite "both_sides_times1" )"1" expand "index" )"1" replace -1 -2 rl)"1" "1" "1" "1" "1" assert )"1" "gcd_1_nd" )"1" "1" rewrite "gcd_sym" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subgroups" )"2" "P!1" "G!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "K!1" )"2" (hide -1)"2" (lemma "finite_subgroups" )"2" (inst -1 "K!1" "G!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide (- 2))"3" (lemma "left_cosets_partition[T,*,one]" )"3" (inst?)"3" (expand "finite_partition?" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide (- 2))"4" expand * "nonempty?" "empty?" "member" "left_cosets" )"4" (inst?)"4" (inst 1 "one" )"1" (rewrite "left_coset_one" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil )"5" (hide (- 2))"5" (lemma "alt_is_action[T,*,one]" )"5" (inst?) nil nil )) nil ))nil ))nil )"2" (hide (- 2))"2" (skosimp)"2" (expand * "left_cosets" "alt" )"2" (typepred "x1!1`2" )"2" (expand "left_cosets" )"2" (skosimp)"2" (replaces -1)"2" "x1!1`1 * a!1" )"1" rewrite "left_coset_assoc" )nil nil )"2" rewrite "product_in" )"2" "2" "x1!1`1" "K!1" )"2" "2" expand *"subgroup?" "subset?" "member" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (rewrite "T_is_group" ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )nil sylow_theorems nil )nil p_groups nil )"posint" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil group_action nil )"set" sets nil )nil group "algebra/" )nil cosets "algebra/" )"(G!1)" sylow_theorems nil )"[(K!1), (left_cosets[T, *, one](G!1, P!1))]" sylow_theorems nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )nil number_fields nil )nil gcd "ints/" )nil general_properties nil )"odd_int" integers nil )nil real_props nil )nil reals nil )"nat" right_left_cosets nil )nil lagrange_index nil )"int" integers nil )nil finite_sets nil )nil sylow_theorems nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"R" extend nil )nil p_groups nil )"(partial_order?[set[T]])" nil )nil group "algebra/" )"posnat" monad "algebra/" )nil sylow_theorems nil )nil right_left_cosetsnil )"{y | x * y = one AND y * x = one}" group"algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil finite_sets_card_eq "finite_sets/" )"bool" sylow_theorems nil )nil finite_sets nil )"(G!1)" sylow_theorems nil )nil finite_sets_eq"finite_sets/" )"{Y: set[T1] | subset?(Y, X)}" group_action nil )"bool" sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil finite_sets nil )"bool" finite_sets nil )"boolean" notequal nil )NOT const-decl "[bool -> bool]" booleans nil )nil right_left_cosets nil )"bool" lagrange_scaf "algebra/" )nil cosets "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )nil p_groups nil )nil group_action nil )nil naturalnumbers nil )"set[T]" p_groups nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"setofsets[T]" right_left_cosets nil )nil sets nil )nil defined_types nil )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"finite_group[T, *, one]" sylow_theoremsnil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3531324060"" (skosimp*)"" (hide -)"" (typepred "G!1" )"" (expand "finite_group?" )"" (flatten)"" (hide -1)"" (lemma "powerset_finite[T]" )"" (inst?)"" (lemma "finite_subset[set[T]]" )"" "powerset[T](G!1)" "p_subgroup_sylow(G!1, p!1)" )"" (assert )"" (hide (- 2))"" (expand * "subset?" "member" )"" (skosimp)"" expand "p_subgroup_sylow" )"" expand "extend" )"" "" "" expand "subgroup?" )"" "" "" expand "powerset" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"finite_group[T, *, one]" sylow_theoremsnil )"bool" finite_sets nil )nil finite_sets nil )"(nonempty?[set[T]])" nil )nil defined_types nil )nil sets nil )"setofsets" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" primes "ints/" )"setofsets[T]" sylow_theorems nil )"R" extend nil )"bool" group_def "algebra/" )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil finite_sets nil )nil finite_sets_of_sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sylow_theorems nil )set type-eq-decl nil sets nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil )"bool" group_def "algebra/" )nil group "algebra/" ))nil ))nil 3531324060"" (skosimp*)"" (hide -)"" (lemma "normalizer_is_subgroup[T, *, one]" )"1" (inst?)"1" (assert )"1" (lemma "subgroup_is_group[T, *, one]" )"1" (inst?)"1" (assert ) nil nil )"2" (hide (-1 2))"2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil group "algebra/" )nil sylow_theorems nil )"{S: set[T] | subset?(S, G)}" nil )"bool" sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )"set" sets nil )nil normalizer_centralizernil )nil sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )"T" sylow_theorems nil ))nil ))nil 3531324107"" (skosimp*)"" (skoletin* 1 "!1" )"1" case "stabilizer[T,*,one, set[T]](G!1, p_subgroup_sylow(G!1, p!1))(action_by_c(G!1,p_subgroup_sylow(G!1,p!1)), P!1) = normalizer(G!1, P!1)" )"1" case "orbit[T, *, one, set[T]](G!1,p_subgroup_sylow(G!1, p!1))(action_by_c(G!1, p_subgroup_sylow(G!1, p!1)), P!1) = p_subgroup_sylow(G!1, p!1)" )"1" (lemma "orbits_eq_index[T, *, one, set[T]]" )"1" (inst?)"1" (split -1)"1" (prop)"1" (assert ) nil nil )"2" (replaces -2)"2" (replaces -2)"2" (replace -2 -1 rl)"2" (hide -2)"2" (lemma "p_subgroup_sylow_order" )"2" "m!1" "n!1" "p!1" "G!1" "P!1" )"2" assert )"2" "Lagrange_index[T,*,one]" )"2" "G!1" "normalizer(G!1, P!1)" )"1" "normalizer(G!1, P!1)" "P!1" )"1" "1" "1" "1" "1" "1" rewrite "commutative_mult" )"1" rewrite "associative_mult" )"1" rewrite "both_sides_times1" )"1" "1" rewrite "commutative_mult" )"1" expand "divides" )"1" "1" "1" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" expand "subgroup?" 1)"3" "subset_of_normalizer[T, *, one]" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "normalizer_is_subgroup[T, *, one]" )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "P!1" )"2" "2" "finite_subgroups[T, *, one]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "normalizer_is_subgroup[T, *, one]" )"3" "3" assert )"3" "finite_subgroups[T, *, one]" )"3" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "T_is_group" )nil nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "finite_subgroups[T, *, one]" )"2" "1" (assert ) nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -2 -3))"3" (lemma "Fix_congruence[T,*,one, set[T]]" )"3" "P!1" "p_subgroup_sylow(G!1, p!1)" "n!1" "p!1" "action_by_c(P!1,p_subgroup_sylow(G!1,p!1))" )"1" (prop)"1" (replace -2 -1 rl)"1" "Fix(P!1, p_subgroup_sylow(G!1, p!1))(action_by_c(P!1, p_subgroup_sylow(G!1, p!1))) = singleton(P!1)" "1" rewrite "card_extend[setof[T], subgroup[T, *, one](G!1)]" )"1" rewrite "card_singleton" )nil nil ))nil )"2" "2" "1" "1" "1" expand "Fix" )"1" expand "extend" )"1" expand "p_subgroup_sylow" "1" expand "extend" )"1" "1" "1" expand *"action_by_c" "singleton" )"1" "p_subgroup_sylow_order" )"1" "m!1" "n!1" "p!1" "G!1" "P!1" )"1" assert )"1" "p_group_iff_power[T,*,one]" )"1" "p!1" "P!1" )"1" assert )"1" "1" "1" case "subgroup?(P!1, normalizer[T,*,one](G!1, x!1))" )"1" "Lagrange" )"1" "normalizer[T, *, one](G!1, x!1)" "P!1" )"1" "G!1" "normalizer[T, *, one](G!1, x!1)" )"1" assert )"1" "1" expand "divides" )"1" "1" replace "1" "1" "1" "both_sides_times2" )"1" "p!1 ^ n!1" "m!1" "x!3 * x!2" )"1" assert )"1" "1" "gcd_1_gcd_1" )"1" "m!1" "p!1" "x!3" "x!2" )"1" rewrite "gcd_sym" )"1" assert )"1" "1" "1" rewrite "gcd_sym" )"1" "Second_Sylow_Theorem" )"1" "x!3" "n!1" "p!1" "normalizer[T, *, one](G!1, x!1)" "x!1" "P!1" )"1" assert )"1" "1" "1" "1" "1" expand "is_conjugate" )"1" "1" "normal_in_normalizer[T, *, one]" )"1" "1" "1" expand "normal_subgroup?" )"1" "1" "normal_prep[T, *, one]" )"1" "normalizer[T, *, one](G!1, x!1)" "x!1" )"1" "1" "1" "a!2" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "p_subgroup_sylow?" )"2" "2" "1" assert )nil nil )"2" "H!1" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "2" "subgroup_transitive[T, *, one]" )"2" "G!1" "normalizer[T, *, one](G!1, x!1)" "H!1" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "p_subgroup_sylow?" )"2" "2" assert )"2" "2" "1" assert )nil nil )"2" "H!1" )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "2" "subgroup_transitive[T, *, one]" )"2" "G!1" "normalizer[T, *, one](G!1, x!1)" "H!1" )"1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subgroup?" "2" "subset_of_normalizer[T, *, one]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "finite_subgroups[T, *, one]" )"3" "normalizer[T, *, one](G!1, x!1)" "G!1" )"1" assert )"1" "1" "normalizer_is_subgroup[T, *, one]" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "T_is_group" )nil nil ))nil )"5" "5" "order(normalizer[T, *, one](G!1, x!1))" )"5" "5" "prime_gt_1" )"5" "5" assert )"5" "5" "expt_pos" )"5" "5" expand *">=" ">" )"5" "pos_times_lt" )"5" "p!1 ^ n!1" "x!3" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "2" "finite_subgroups[T, *, one]" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil )"2" "2" "normalizer_is_subgroup[T, *, one]" )"2" "2" assert )"2" "2" "finite_subgroups[T, *, one]" )"2" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "T_is_group" )nil nil ))nil ))nil ))nil )"2" "2" expand *"subgroup?" "subset?" "member" )"2" "2" expand "normalizer" )"2" expand "extend" )"2" "1" "inv(x!2)" )"1" rewrite "inv_inv" )nil nil )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil )"2" "P!1" )"2" "2" expand *"subgroup?" "subset?" "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "normalizer_is_subgroup[T, *, one]" )"3" "3" assert )"3" "3" "subgroup_is_group[T, *, one]" )"3" "1" assert )nil nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "P!1" )"2" "2" "finite_subgroups[T, *, one]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "2" expand * "singleton" "Fix" )"2" expand "extend" )"2" "1" "1" expand "action_by_c" )"1" "1" "1" "g!1" )"1" "lc_is_eq[T, *, one]" )"1" "G!1" "P!1" "g!1" "one" )"1" assert )"1" "1" rewrite "left_coset_one" )"1" "1" "rc_is_eq[T, *, one]" )"1" "G!1" "P!1" "inv[T, *, one](g!1)" "one" )"1" assert )"1" "1" rewrite "right_coset_one" )nil nil )"2" "2" "inv[T, *, one](g!1)" )"2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "p_subgroup_sylow" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (- 2))"2" (typepred "P!1" )"2" "2" "finite_subgroups[T, *, one]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (lemma "p_subgroup_sylow_order" )"3" "m!1" "n!1" "p!1" "G!1" "P!1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" (lemma "Third_Sylow_Theorem_TCC1" )"4" "m!1" "n!1" "p!1" "G!1" "P!1" )"4" (assert ) nil nil )) nil ))nil )"5" (hide-all-but (-5 1))"5" expand * "nonempty?" "empty?" "member" )"5" "P!1" )"5" expand "p_subgroup_sylow" )"5" expand "extend" )"5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (hide (- 2))"6" (expand "group_action?" )"6" "6" "1" expand "action_by_c" )"1" rewrite "left_coset_one" )"1" rewrite "inv_one" )"1" rewrite "right_coset_one" )nil nil ))nil ))nil ))nil )"2" expand "action_by_c" )"2" rewrite "inv_star" )"2" rewrite "right_coset_assoc" "2" rewrite "left_coset_assoc" "2" rewrite "lr_coset_assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (skosimp)"2" (expand "action_by_c" )"2" expand "p_subgroup_sylow" )"2" expand "extend" )"2" "conjugate_is_subgroup[T, *, one]" )"2" "G!1" "x1!1`1" "x1!1`2" )"1" "subgroup_is_group[T, *, one]" )"1" "1" assert )"1" "x1!1`2" )"1" "1" expand "p_subgroup_sylow" )"1" expand "extend" )"1" "1" "1" "conjugate_is_p_subgroup_sylow" )"1" "m!1" "n!1" "p!1" "G!1" "x1!1`2" )"1" assert )"1" "x1!1`1" )"1" "1" "x1!1`1" "P!1" )"1" "1" expand *"subgroup?" "subset?" "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x1!1`2" )"2" expand "p_subgroup_sylow" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil ))nil ))nil )"3" "3" "x1!1`1" "P!1" )"3" "3" expand *"subgroup?" "subset?" "member" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (- 2))"3" (typepred "P!1" )"3" (hide -1)"3" "finite_subgroups[T, *, one]" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -3 2))"2" (lemma "Third_Sylow_Theorem_TCC1" )"2" (inst -1 "m!1" "n!1" "p!1" "G!1" "P!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide (-1 -2 -3 2))"3" (expand "group_action?" )"3" (skosimp*)"3" (prop)"1" (expand "action_by_c" )"1" (rewrite "left_coset_one" )"1" (rewrite "inv_one" )"1" rewrite "right_coset_one" )nil nil ))nil ))nil ))nil )"2" (expand "action_by_c" )"2" (rewrite "inv_star" )"2" (rewrite "right_coset_assoc" :dir rl)"2" rewrite "left_coset_assoc" :dir rl)"2" rewrite "lr_coset_assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2))"2" (decompose-equality 1)"1" (iff)"1" (prop)"1" (expand "orbit" )"1" (expand "extend" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand * "orbit" "extend" )"2" (assert )"2" (expand "action_by_c" )"2" (expand "p_subgroup_sylow" )"2" (expand "extend" )"2" (prop)"2" "2" "Second_Sylow_Theorem" )"2" "m!1" "n!1" "p!1" "G!1" "P!1" "x!1" )"2" assert )"2" "2" expand "p_subgroup_sylow?" )"2" "2" "2" assert )"2" "2" "2" expand "is_conjugate" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -) (("2" (rewrite "T_is_group" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide (- 2))"2" (decompose-equality 1)"1" (iff)"1" (prop)"1" (expand * "stabilizer" "normalizer" )"1" (expand "extend" )"1" (prop)"1" (hide (-1 -2))"1" (expand "action_by_c" )"1" (replace -1 1 rl)"1" (rewrite "lr_coset_assoc" )"1" rewrite "lr_coset_assoc" )"1" rewrite "lr_coset_assoc" )"1" rewrite "right_coset_assoc" )"1" rewrite "right_coset_one" )"1" rewrite "left_coset_assoc" )"1" rewrite "left_coset_one" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "stabilizer" "normalizer" )"2" (expand "extend" )"2" (prop)"2" (hide (-1 -2))"2" (expand "action_by_c" )"2" (replace -1 1 rl)"2" (rewrite "lr_coset_assoc" )"2" rewrite "lr_coset_assoc" )"2" rewrite "lr_coset_assoc" )"2" rewrite "right_coset_assoc" )"2" rewrite "right_coset_one" )"2" rewrite "left_coset_assoc" )"2" rewrite "left_coset_one" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "T_is_group" ) nil nil ))nil ))nil )"3" (hide (- 2)) (("3" (rewrite "T_is_group" ) nil nil )) nil )"4" (hide-all-but (-5 1))"4" (expand "p_subgroup_sylow" )"4" (expand "extend" ) (("4" (propax) nil nil )) nil ))nil ))nil )"5" (hide (-1 2))"5" (skosimp)"5" (expand "p_subgroup_sylow" 1 1)"5" (expand "extend" )"5" (prop)"1" (hide (-1 -2))"1" (expand "action_by_c" )"1" (typepred "x1!1`2" )"1" (expand "p_subgroup_sylow" )"1" (expand "extend" )"1" (prop)"1" "1" "conjugate_is_p_subgroup_sylow" )"1" "m!1" "n!1" "p!1" "G!1" "x1!1`2" )"1" assert )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "action_by_c" )"2" (lemma "conjugate_is_subgroup[T, *, one]" )"1" (inst?)"1" (hide-all-but (-1 1))"1" (lemma "subgroup_is_group[T, *, one]" )"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide (- 2))"2" (typepred "x1!1`2" )"2" (expand "p_subgroup_sylow" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (- 2))"2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil )"3" (hide -)"3" (expand "action_by_c" )"3" (lemma "conjugate_is_subgroup[T, *, one]" )"1" (inst?)"1" (hide 2)"1" (typepred "x1!1`2" )"1" expand "p_subgroup_sylow" )"1" expand "extend" )"1" (prop) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide -)"2" (lemma "normalizer_is_subgroup[T, *, one]" )"1" (inst?)"1" (assert )"1" (lemma "subgroup_is_group[T, *, one]" )"1" (inst?)"1" (assert ) nil nil )"2" (hide (- 2))"2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*)"3" (hide -) (("3" (rewrite "T_is_group" ) nil nil )) nil ))nil ))nil ))nil )"setofsets[T]" sylow_theorems nil )nil sets nil )"bool" primes "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil group "algebra/" )"bool" group_def "algebra/" )"T" sylow_theorems nil )"[T, T -> T]" sylow_theorems nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sylow_theorems nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil finite_sets nil )"nat" finite_sets nil )"[bool, bool -> bool]" booleans nil )"{n: nat | n = Card(S)}" finite_sets nil )"bool" group_def "algebra/" )"set" sets nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" sets nil )"{S: set[T] | subset?(S, G)}" nil )"[bool, bool -> bool]" booleans nil )"nat" right_left_cosets nil )"bool" divides nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" exponentiation nil )"[(G!1), (p_subgroup_sylow(G!1, p!1))]" nil )nil group "algebra/" )nil group "algebra/" )"{Y: set[T1] | subset?(Y, X)}" group_action nil )nil lagrange_index nil )nil normalizer_centralizer nil )"(partial_order?[set[T]])" nil )nil normalizer_centralizernil )"nonneg_int" nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )nil sylow_theorems nil )nil number_fields nil )nil group "algebra/" )"subgroup[T, *, one](G!1)" sylow_theoremsnil )"finite_group[T, *, one]" sylow_theoremsnil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil sylow_theorems nil )nil group_action nil )"[(P!1), (p_subgroup_sylow(G!1, p!1))]" nil )"set[T]" cosets "algebra/" )nil sylow_theorems nil )nil groups_scaf nil )"(singleton?)" sets nil )"bool" sets nil )"R" extend nil )"bool" booleans nil )"{Y: set[T1] | subset?(Y, X)}" group_action nil )"finite_set[T]" nil )"(nonempty?[T])" nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )nil finite_sets nil )nil extend_set_props nil )"setof[T]" sylow_theorems nil )nil sylow_theorems nil )nil real_types nil )nil real_types nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil primes "ints/" )"posnat" monad "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )"subgroup[T, *, one](normalizer[T, *, one](G!1, x!1))" nil )"boolean" normal_subgroups "algebra/" )nil normal_subgroups "algebra/" )nil normalizer_centralizer nil )"bool" sylow_theorems nil )"bool" sylow_theorems nil )"subgroup[T, *, one](normalizer[T, *, one](G!1, x!1))" nil )nil groups_scaf nil )"int" sylow_theorems nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil gcd "ints/" )nil general_properties nil )nil real_props nil )nil lagrange "algebra/" )"bool" sets nil )nil group "algebra/" )nil group "algebra/" )"T" sylow_theorems nil )"{y | x * y = one AND y * x = one}" group"algebra/" )nil group "algebra/" )nil p_groups nil )nil cosets "algebra/" )"(P!1)" sylow_theorems nil )nil group "algebra/" )nil cosets "algebra/" )nil cosets "algebra/" )nil group "algebra/" )nil cosets "algebra/" )"odd_int" integers nil )nil sylow_theorems nil )"bool" sets nil )"bool" sets nil )"bool" group_action nil )nil group "algebra/" )nil group "algebra/" )nil cosets "algebra/" )nil cosets "algebra/" )nil cosets "algebra/" )"set[T]" cosets "algebra/" )"posnat" sylow_theorems nil )nil group_action nil )"set[T]" sylow_theorems nil )"{S: set[T] | subset?(S, G)}" group_actionnil )nil group_action nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.632Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-05)
¤ *Bot Zugriff
2026-05-26
