Quelle p_groups.prf
Sprache: Lisp
(p_groupsnil 3530721851"" (rewrite "fullset_is_group" ) nil nil )nil p_groups nil )) nil ))nil 3530273648 ("" (subtype-tcc) nil nil ) nil nil ))nil 3530265242"" (skosimp*)"" (typepred "x1!1`2" "x1!1`1" "H!1" )"" (expand "subgroup?" )"" (expand * "subset?" "member" )"" (inst?)"" (assert )"" (hide -3)"" (expand "left_cosets" )"" (skosimp)"" (expand "alt" )"" (inst 1 "x1!1`1 * a!1" )"1" (replaces -1)"1" (rewrite "left_coset_assoc" ) nil nil ))nil )"2" (rewrite "product_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setofsets[T]" right_left_cosets nil )nil sets nil )nil defined_types nil )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil group "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"set[T]" p_groups nil )nil group "algebra/" )nil cosets "algebra/" )"group[T, *, one]" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )"[(H!1), (left_cosets(G!1, K!1))]" p_groupsnil )"(G!1)" p_groups nil ))nil ))nil 3530282276"" (skosimp*)"" (expand "group_action?" )"" (skosimp*)"" (prop)"1" (expand "alt" )"1" (rewrite "left_coset_one" ) nil nil )) nil )"2" (expand "alt" )"2" (rewrite "left_coset_assoc" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" group_action nil )nil cosets "algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil sets nil )"setofsets[T]" right_left_cosets nil )nil p_groups nil )"[T, T -> T]" p_groups nil )"T" p_groups nil )"set[T]" p_groups nil )nil cosets "algebra/" ))nil 3530282442"" (skosimp*)"" (expand * "subset?" "member" "Fix" "alt" )"" (expand "extend" )"" (prop)"1" (skosimp)"1" (inst -2 "x!1" )"1" (rewrite "left_coset_assoc" )"1" (lemma "lc_eq" )"1" (inst -1 "G!1" "K!1" "x!1 * g!1" "g!1" )"1" (assert )"1" (skosimp)"1" (hide (-2 -3 -4))"1" (expand "*" 1)"1" (inst 1 "g!1 * h!1" )"1" replace -1 1 rl)"1" rewrite "assoc" :dir rl)nil nil ))nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "g!2" )"2" (inst?)"2" (assert )"2" (expand "*" -3)"2" (skosimp)"2" (hide -1)"2" (rewrite "left_coset_assoc" )"2" (lemma "lc_is_eq" )"2" "G!1" "K!1" "g!2 * g!1" "g!1" )"2" assert )"2" "inv(g!1) * h!1" )"1" "1" "1" rewrite "assoc" )"1" rewrite "assoc" :dir rl)nil nil ))nil ))nil ))nil )"2" "2" "h!1" )"2" "2" "2" "h!2" )"2" rewrite "assoc" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1)"3" (expand "left_cosets" ) (("3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"set[T]" p_groups nil )"{Y: set[T1] | subset?(Y, X)}" group_action nil )"bool" sets nil )"T" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )nil group "algebra/" )"group[T, *, one]" p_groups nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil p_groups nil )nil cosets "algebra/" )"subgroup[T, *, one](G!1)" p_groups nil )"[T, T -> boolean]" equalities nil )"(G!1)" p_groups nil )"(K!1)" p_groups nil )nil group "algebra/" )nil monad "algebra/" )"{y | x * y = one AND y * x = one}" group"algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil group "algebra/" )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil cosets "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"({t: T | EXISTS (h: (K!1)): t = g!1 * h})" nil )nil group "algebra/" )nil monad "algebra/" )nil cosets "algebra/" )"setofsets[T]" right_left_cosets nil )"R" extend nil ))nil 3530267101"" (skosimp*)"" (typepred "x1!1`2" "x1!1`1" "H!1" )"" (expand "subgroup?" )"" (expand * "subset?" "member" )"" (inst?)"" (assert )"" (hide -3)"" (expand "left_cosets" )"" (skosimp)"" (expand "alt" )"" (inst 1 "x1!1`1 * a!1" )"1" (replaces -1)"1" (rewrite "left_coset_assoc" ) nil nil ))nil )"2" (rewrite "product_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" group_def "algebra/" )"setofsets[T]" right_left_cosets nil )nil sets nil )nil defined_types nil )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil group "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"set[T]" p_groups nil )nil group "algebra/" )nil cosets "algebra/" )"finite_group[T, *, one]" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )"[(H!1), (left_cosets(G!1, H!1))]" p_groupsnil )"(G!1)" p_groups nil ))nil ))nil 3530285250"" (skosimp*)"" (lemma "Fix_iff_subset" )"" (inst -1 "G!1" "H!1" "H!1" "g!1" )"" (assert )"" (prop)"1" (hide (-1 -2))"1" (lemma "left_coset_correspondence_inv[T, *, one]" )"1" (inst -1 "G!1" "H!1" "g!1" )"1" (assert )"1" (typepred "H!1" )"1" (hide -1)"1" (lemma "finite_subgroups" )"1" (inst?)"1" (assert )"1" "1" expand "finite_group?" )"1" "card_eq_bij[T, T]" )"1" "H!1" "g!1 * H!1 * inv(g!1)" )"1" "1" "1" rewrite "same_card_subset" )nil nil ))nil ))nil )"2" "2" "bijection_finite_set2[T,T]" )"2" "H!1" "g!1 * H!1 * inv(g!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (1 3))"2" (replace -1 1 rl)"2" (hide -1)"2" (rewrite "subset_reflexive" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_groups nil )"(partial_order?[set[T]])" nil )"bool" sets nil )nil sets_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )"bool" finite_sets nil )"finite_group[T, *, one]" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(G!1)" p_groups nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil finite_sets nil )nil finite_sets nil )nil finite_sets_eq"finite_sets/" )nil finite_sets_card_eq "finite_sets/" )nil right_left_cosetsnil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil p_groups nil ))nil 3530352745"" (skosimp*)"" (lemma "finite_subgroups" )"" (inst -1 "H!1" "G!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3530352927"" (skosimp*)"" (hide -1)"" (expand "p_group?" )"" (skosimp)"" (inst -1 "a!1" )"1" (skosimp)"1" (inst?)"1" (replace -1 1 rl)"1" (hide -1)"1" (expand "period" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "a!1" "H!1" )"2" (hide -2)"2" (expand "subgroup?" )"2" (expand "subset?" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"posnat" finite_groups "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 naturalnumbers nil )nil p_groups nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" p_groups nil )"T" p_groups nil )"bool" group_def "algebra/" )nil group "algebra/" )"finite_group[T, *, one]" p_groups nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T, *, one](G!1)" p_groups nil )"(H!1)" p_groups nil )"bool" p_groups nil ))nil 3530273648 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3530719670"" (skosimp*)"" (prop)"1" (lemma "prime_factors" )"1" (inst -1 "order(G!1)" )"1" (skosimp)"1" (lemma "product_only_power" )"1" (inst -1 "fs!1" "p!1" )"1" (prop)"1" (skosimp)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (hide -3)"2" expand * "only_power_p" "p_group?" "list_of_primes?" )"2" (skosimp)"2" "divides_product" )"2" "fs!1" "j!1" )"2" "j!1" )"2" replace -2 -1 rl)"2" "2" "cauchy" )"2" "2" assert )"2" "2" "x!1" )"2" "2" "2" 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" (skosimp)"2" (expand "p_group?" )"2" (skosimp)"2" (lemma "Lagrange" )"2" (inst -1 "G!1" "generated_by(a!1)" )"1" (prop)"1" (replaces -2)"1" (lemma "divides_prime_power" )"1" (inst?)"1" (assert )"1" (skosimp)"1" (hide -1)"1" "period_is_generated_order" )"1" "1" assert )"1" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "generated_is_subgroup" ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "finite_group?" )"2" (lemma "finite_generated_by" )"2" (inst -1 "G!1" "a!1" )"2" (assert ) 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 )nil p_groups nil )set type-eq-decl nil sets nil )"[T, T -> T]" p_groups nil )"T" p_groups nil )"bool" monad_def "algebra/" )nil monad "algebra/" )"posnat" monad "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )nil general_properties nil )"posint" exponentiation nil )"bool" prime_factorization"numbers/" )nil naturalnumbers nil )"bool" reals nil )nil cauchy nil )nil general_properties nil )"bool" general_properties nil )"bool" prime_factorization "numbers/" )"bool" p_groups nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil prime_factorization "numbers/" )nil lagrange "algebra/" )nil finite_groups "algebra/" )nil general_properties nil )"bool" sets nil )nil finite_groups"algebra/" )nil cyclic_group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"group" group "algebra/" )"finite_group[T, *, one]" p_groups nil )"(G!1)" p_groups nil ))nil 3530567198"" (skosimp*)"" (typepred "G!1" "H!1" )"" (hide -2)"" (lemma "finite_subgroups" )"" (inst -1 "H!1" "G!1" )"" (assert )"" (lemma "index_divides" )"" (inst?)"" (assert )"" (lemma "p_group_iff_power" )"" (inst?)"" (assert )"" (skosimp)"" (replaces -1)"" "divides_prime_power" )"" "1" assert )"1" "1" "1" "i!1 = 0" "1" rewrite "expt_x0" )"1" "Lagrange_index" )"1" "1" assert )"1" "1" rewrite "identity_mult" )"1" "orders_equal" )"1" "G!1" "H!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "divides_power" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "index_gt1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil p_groups nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil group "algebra/" )nil p_groups nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"nat" right_left_cosets nil )"finite_group[T, *, one]" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil )"[T, T -> boolean]" equalities nil )nil lagrange_index nil )"posnat" monad "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil number_fields nil )nil number_fields nil )nil finite_groups "algebra/" )nil exponentiation nil )nil general_properties nil )"posint" exponentiation nil )nil right_left_cosets nil )"(total_order?[real])" nil )nil general_properties 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 lagrange_index nil ))nil 3530273648"" (skosimp*)"" (lemma "center_subgroup" )"" (inst?)"" (expand "normal_subgroup?" )"" (assert )"" (expand "subgroup?" )"" (assert )"" (skosimp)"" (expand * "subset?" "member" )"" (skosimp)"" (hide -1)"" (expand "*" )"" (skosimp)"" (typepred "h!1" )"" "" "h!2" )"" expand "center" )"" expand "extend" )"" "1" "1" "1" "1" "1" "a!1" )"1" rewrite "assoc" "1" replace -2 1 rl)"1" rewrite "assoc" )"1" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "product_in" )"2" rewrite "product_in" )"2" rewrite "inv_in" )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 )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )nil group "algebra/" )"boolean" normal_subgroups "algebra/" )"bool" group_def "algebra/" )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"{s: set[T] | subset?(s, G)}" group "algebra/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"R" extend nil )nil group "algebra/" )nil group "algebra/" )nil monad "algebra/" )nil group "algebra/" )nil group "algebra/" )"bool" sets nil )"bool" sets nil )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3530273648"" (skosimp*)"" (inst 1 "one" )"1" (rewrite "left_coset_one" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil )"group[T, *, one]" p_groups nil )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil p_groups nil )"{s: set[T] | subset?(s, G)}" group "algebra/" )"bool" sets nil )nil cosets "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" ))nil ))nil 3530721851"" (skosimp*)"" (rewrite "left_cosets_group" )"" (hide 2)"" (lemma "center_is_normal[T, *, one]" )"1" (inst?)"1" (assert )"1" (expand "normal_subgroup?" )"1" (flatten)"1" (hide -2)"1" (expand "subgroup?" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "fullset_is_group" ) nil nil ))nil ))nil ))nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans 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/" )"bool" sets nil )"{s: set[T] | subset?(s, G)}" group "algebra/" )nil p_groups nil )"[T, T -> T]" p_groups nil )"T" p_groups nil )nil groups_scaf nil )"set" sets nil )"bool" group_def "algebra/" )nil p_groups nil ))nil ))nil 3530384047"" (skosimp*)"" (lemma "center_is_normal[T, *, one]" )"1" (inst?)"1" (expand "cyclic?" )"1" (skosimp)"1" (typepred "a!1" )"1" (skosimp)"1" (decompose-equality -4)"1" (hide -3)"1" (expand "abelian_group?" )"1" (expand * "commutative?" "restrict" )"1" (skosimp)"1" (inst-cp -1 "x!1 * center(G!1)" )"1" (iff)"1" "1" "1" "y!1 * center(G!1)" )"1" "1" "1" "1" expand "generated_by" )"1" "1" "1" "coset_power_int[T,*,one]" )"1" "G!1" "i!1" "a!2" "center(G!1)" )"1" "G!1" "i!2" "a!2" "center(G!1)" )"1" "1" "1" "lc_eq" )"1" "G!1" "center(G!1)" "y!1" "a!2 ^ i!1" )"1" "G!1" "center(G!1)" "x!1" "a!2 ^ i!2" )"1" expand "normal_subgroup?" )"1" "1" assert )"1" "1" "1" "1" "1" "h!1" "h!2" )"1" expand *"center" "extend" )"1" "1" "1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "assoc" "1" "a!2 ^ i!1" )"1" replace "1" "1" rewrite "assoc" "1" rewrite "assoc" "1" "h!1" )"1" "1" rewrite "assoc" "1" rewrite "assoc" "1" "a!2 ^ i!2" )"1" replace "1" "1" rewrite "assoc" "1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "assoc" )"1" rewrite "expt_mult" )"1" rewrite "expt_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "expt_member" )"2" "G!1" "a!2" "i!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "h!1" )"2" expand *"center" "extend" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "expt_member" )"2" "G!1" "a!2" "i!1" )"2" 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" expand "/" )"2" expand "restrict" )"2" expand "left_cosets" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (inst 1 "y!1" ) nil nil ))nil ))nil ))nil )"2" "2" expand "/" )"2" expand "restrict" )"2" expand "left_cosets" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (inst 1 "x!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (rewrite "left_cosets_group" ) nil nil )) nil )"3" (hide-all-but 1)"3" (inst 1 "one" )"1" (rewrite "left_coset_one" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "fullset_is_group" ) nil nil )) nil ))nil ))nil )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups 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 )"boolean" group "algebra/" )"group[left_cosets(G, N), mult(G, N), N]" nil )"left_cosets(G, H)" factor_groups "algebra/" )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil cosets "algebra/" )"{s: set[T] | subset?(s, G)}" group "algebra/" )"bool" sets nil )"set[T]" cosets "algebra/" )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"group" group "algebra/" )"bool" group_def "algebra/" )"setofsets[T]" right_left_cosets nil )nil groups_scaf nil )"T" group "algebra/" )"R" extend nil )"(G!1)" p_groups nil )"int" p_groups nil )"bool" sets nil )nil group "algebra/" )"int" integers nil )nil group "algebra/" )"int" p_groups nil )"(center(G!1))" p_groups nil )nil group "algebra/" )nil cosets "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 )"(G!1)" p_groups nil )"(G!1)" p_groups nil )"group[T, *, one]" p_groups nil )"bool" operator_defs nil )"R" restrict nil )nil factor_groups "algebra/" )nil cosets "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )nil group "algebra/" )nil p_groups nil ))nil 3530273648"" (skosimp*)"" (typepred "H!1" "G!1" )"" (hide (-1 -4))"" (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" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil p_groups nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil group "algebra/" ))nil ))nil 3530273648"" (skosimp*)"" (lemma "normalizer_is_subgroup" )"" (inst?)"" (assert )"" (hide (-2 -3 -4))"" (lemma "finite_subgroups" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )nil normalizer_centralizernil )nil group "algebra/" )"{S: set[T] | subset?(S, G)}" nil )"bool" sets nil )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 booleans nil )nil booleans nil ))nil ))nil 3530273648"" (skosimp*)"" (hide-all-but 1)"" (lemma "normal_in_normalizer" )"" (inst?)"" (assert )"" (expand "normal_subgroup?" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans 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/" )"boolean" normal_subgroups "algebra/" )nil normalizer_centralizer nil )nil p_groups nil )"[T, T -> T]" p_groups nil )"T" p_groups nil ))nil ))nil 3530541504"" (skosimp*)"" (lemma "p_group_iff_power" )"" (inst?)"" (assert )"" (skosimp)"" (lemma "Fix_congruence[T,*,one,set[T]]" )"" "H!1" "left_cosets(G!1,H!1)" "m!1" "p!1" "alt(G!1,H!1,H!1)" )"1" (prop)"1" (expand "index" )"1" "Fix(H!1, left_cosets(G!1, H!1))(alt(G!1, H!1, H!1)) = left_cosets(normalizer(G!1, H!1), H!1)" "1" (hide (-2 -3 -4))"1" (expand "divides" )"1" (skosimp*)"1" (inst 1 "x!2 - x!1" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" "1" expand "Fix" -1)"1" expand "extend" )"1" "1" "1" expand "left_cosets" -1)"1" "1" "1" "Fix_iff_subset_cor" )"1" "G!1" "H!1" "H!1" "a!1" )"1" assert )"1" "1" expand "left_cosets" )"1" "1" expand "normalizer" )"1" expand "extend" )"1" replace "1" rewrite "lr_coset_assoc" )"1" rewrite "left_coset_assoc" )"1" rewrite "left_coset_one" )"1" rewrite "right_coset_assoc" )"1" rewrite "right_coset_one" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "left_cosets" -1)"2" "2" "a!1" )"2" "2" expand "normalizer" )"2" expand "extend" )"2" "2" "2" "Fix_iff_subset_cor" )"2" "G!1" "H!1" "H!1" "a!1" )"2" assert )"2" "2" replace "2" rewrite "lr_coset_assoc" )"2" rewrite "left_coset_assoc" )"2" rewrite "left_coset_one" )"2" rewrite "right_coset_assoc" )"2" rewrite "right_coset_one" )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" (typepred "G!1" "H!1" )"2" (hide -2)"2" (lemma "finite_subgroups" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "left_cosets_partition" )"3" (inst?)"3" (expand "finite_partition?" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (expand "nonempty?" )"4" (expand * "empty?" "member" )"4" (inst -1 "H!1" )"4" (expand "left_cosets" )"4" (inst 1 "one" )"1" (rewrite "left_coset_one" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (lemma "alt_is_action" )"5" (inst?) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (expand "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" "H!1" )"2" "2" expand "subgroup?" )"2" expand *"subset?" "member" )"2" "2" (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 p_groups nil )nil group_action nil )nil group "algebra/" )"(G!1)" p_groups nil )"[(H!1), (left_cosets(G!1, H!1))]" p_groupsnil )"{S: set[T] | subset?(S, G)}" nil )"{Y: set[T1] | subset?(Y, X)}" group_action nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"bool" divides nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"odd_int" integers nil )"(G!1)" p_groups nil )"{y | x * y = one AND y * x = one}" group"algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil cosets "algebra/" )nil cosets "algebra/" )nil cosets "algebra/" )nil cosets "algebra/" )nil group "algebra/" )nil cosets "algebra/" )"set[T]" cosets "algebra/" )"bool" sets nil )nil p_groups nil )"R" extend nil )nil group "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"nat" right_left_cosets nil )nil group "algebra/" )nil right_left_cosets nil )"bool" lagrange_scaf "algebra/" )"bool" sets nil )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )"bool" sets nil )nil p_groups nil )nil group_action nil )nil naturalnumbers nil )"set[T]" p_groups nil )"setofsets[T]" right_left_cosets nil )nil sets nil )nil defined_types nil )"subgroup[T, *, one](G!1)" p_groups nil )"finite_group[T, *, one]" p_groups nil )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil p_groups 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 3530548859"" (skosimp*)"" (lemma "Lagrange" )"" (inst -1 "normalizer(G!1, H!1)" "H!1" )"1" (prop)"1" (lemma "divisor_smaller" )"1" (inst?)"1" (prop)"1" (hide-all-but -1)"1" (lemma "index_gt1" )"1" (inst -1 "normalizer(G!1, H!1)" "H!1" )"1" (assert ) nil nil )"2" (lemma "normal_in_normalizer" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (lemma "normalizer_is_subgroup" )"3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "<=" )"2" (prop)"1" (hide-all-but (-1 -5))"1" (expand "order" ) (("1" (assert ) nil nil ))nil ))nil )"2" (lemma "index_gt1" )"2" (inst -1 "normalizer(G!1, H!1)" "H!1" )"1" (lemma "prime_gt_1" )"1" (inst?)"1" (assert )"1" "1" case "index(normalizer(G!1, H!1), H!1) > 1" )"1" "1" "Lagrange_index" )"1" "normalizer(G!1, H!1)" "H!1" )"1" "1" "1" "both_sides_times1" )"1" "order(normalizer(G!1, H!1))" "1" "index(normalizer(G!1, H!1), H!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "normal_in_normalizer" )"2" "2" assert )"2" expand "normal_subgroup?" )"2" 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 ))nil ))nil ))nil )"2" "subgroup_is_p_group" )"2" "p!1" "G!1" "H!1" )"2" assert )"2" "2" "normalizer_index" )"2" "2" assert )"2" "1" "divisor_smaller" )"1" "1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "p_divides_index" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "normal_in_normalizer" )"2" (inst?)"2" assert )"2" expand "normal_subgroup?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "normalizer_is_subgroup" )"3" (inst?)"3" assert )"3" "finite_subgroups" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "normal_in_normalizer" )"2" (inst?)"2" (assert )"2" (expand "normal_subgroup?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "H!1" "G!1" )"2" (hide -1)"2" (lemma "finite_subgroups" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "normalizer_is_subgroup" )"3" (inst?)"3" (assert )"3" (lemma "finite_subgroups" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )nil lagrange "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 naturalnumbers nil )"bool" monad_def "algebra/" )nil monad "algebra/" )nil integers nil )"bool" reals nil )nil integers nil )"posnat" monad "algebra/" )"bool" reals nil )nil primes "ints/" )"nat" right_left_cosets nil )nil lagrange_index nil )nil group "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"boolean" notequal nil )nil reals nil )"boolean" normal_subgroups "algebra/" )"(total_order?[real])" nil )nil p_groups nil )nil p_groups nil )nil p_groups nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil normalizer_centralizer nil )nil normalizer_centralizernil )nil right_left_cosets nil )nil divides nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" sets nil )"{S: set[T] | subset?(S, G)}" nil )nil group "algebra/" )"finite_group[T, *, one]" p_groups nil )"subgroup[T, *, one](G!1)" p_groups nil ))nil 3530273648"" (skosimp*)"" (typepred "G!1" )"" (lemma "center_subgroup" )"" (inst?)"" (lemma "finite_subgroups" )"" (inst?)"" (assert )"" (hide (-2 -3))"" expand * "finite_group?" "finite_monad?" "group?" "monoid?" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil p_groups nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" group_def "algebra/" )nil group "algebra/" )"{s: set[T] | subset?(s, G)}" group "algebra/" )"bool" sets nil )"bool" monoid_def "algebra/" )"bool" monad_def "algebra/" )"(strict_total_order?[real])" real_props nil )nil group "algebra/" )nil group "algebra/" ))nil ))nil 3530350714"" (skosimp*)"" (lemma "p_group_iff_power" )"" (inst?)"" (assert )"" (skosimp)"" (case-replace "m!1 = 0" :hide? T)"1" (hide (-3 -4 1))"1" (rewrite "expt_x0" ) (("1" (assert ) nil nil ))nil ))nil )"2" (case-replace "center(G!1) = G!1" :hide? T)"1" (expand ">=" )"1" (replace -1 2)"1" (lemma "prime_gt_1" )"1" (inst -1 "p!1" )"1" (prop)"1" (hide (-2 -3 -4 -5))"1" (lemma "both_sides_expt_gt1_le" )"1" "p!1" "1" "m!1" )"1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "nonempty?(CLs_nc(G!1))" )"1" (lemma "class_equation_2" )"1" (inst?)"1" (lemma "divide_sigma" )"1" (inst -1 "CLs_nc(G!1)" "p!1" )"1" (prop)"1" "ZZ" "sigma_set.sigma(restrict[setof[T], finite_set[T], boolean](CLs_nc(G!1)), card)" )"1" "divides_power" )"1" "1" replace -5 -1 rl)"1" replace -3 -1)"1" "divides_element" )"1" "p!1" "ZZ" "card(center(G!1))" )"1" assert )"1" "1" "order_gt_p[T,*,one]" )"1" "1" expand "order" )"1" nil nil ))nil )"2" "2" "center_subgroup" )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "fullset_is_group" )nil nil ))nil ))nil ))nil )"2" "2" expand "order" )"2" "integers.closed_minus" )"2" "card(G!1)" "card(center(G!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 -5 1))"2" "2" "1" "1" "empty_card[T]" )"1" "1" assert )"1" "1" "A!1" )"1" expand "CLs_nc" )"1" expand "extend" )"1" "1" "1" expand "empty?" )"1" "1" expand "member" )"1" "1" "1" expand "CL" )"1" expand "extend" )"1" "one" )"1" assert )nil nil )"2" rewrite "one_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "A!1" )"2" expand "CLs_nc" )"2" expand "extend" )"2" "2" "2" "2" "CLs_eq_index" )"2" "2" replace -2 -1 rl)"2" "2" "card(A!1) = 0" "1" "1" rewrite "divides_zero" )nil nil ))nil )"2" "divides_prime_power" )"2" "m!1" "p!1" "card(A!1)" )"1" assert )"1" "1" "1" "i!1 = 0" "1" "1" rewrite "expt_x0" )"1" "1" "Lagrange_index" )"1" "1" "1" "1" rewrite "identity_mult" )"1" expand "order" )"1" "same_card_subset[T]" )"1" "centralizer(G!1)(x!1)" "G!1" )"1" assert )"1" "1" "1" "x!1" )"1" expand "member" )"1" expand "center" )"1" expand "extend" )"1" "1" "x!2" )"1" "x!2" )"1" "1" "1" expand "centralizer" )"1" expand "extend" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "centralizer_is_subgroup" )nil nil ))nil ))nil )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "centralizer[T, *, one](G!1)(x!1)" "G!1" )"2" assert )"2" "2" rewrite "centralizer_is_subgroup" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "divides_power" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Lagrange_index" )"2" "1" "1" "1" "1" expand "divides" )"1" nil nil ))nil ))nil ))nil )"2" "2" rewrite "centralizer_is_subgroup" )nil nil ))nil ))nil )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "centralizer[T, *, one](G!1)(x!1)" "G!1" )"2" assert )"2" "2" rewrite "centralizer_is_subgroup" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )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" (lemma "orbits_nFix_is_CLs_nc" )"2" "2" replace -1 1 rl)"2" "2" "G!1" )"2" expand "finite_group?" )"2" "2" "2" "orbits_nFix_partition" )"2" "2" assert )"2" "2" rewrite "a_by_c_is_action" )"2" "2" rewrite "group_is_subgroup" )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))"2" (expand * "nonempty?" "empty?" "member" )"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (hide -2)"1" expand * "center" "extend" )"1" (assert ) nil nil ))nil ))nil )"2" (inst -2 "CL(G!1)(x!1)" )"2" expand "CLs_nc" )"2" expand "extend" )"2" "1" "x!1" )"1" (assert ) nil nil ))nil )"2" expand "CLs" )"2" (inst 1 "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_groups nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil exponentiation nil )nil defined_types nil )"bool" sets nil )nil sets nil )"setofsets[T]" normalizer_centralizer nil )"bool" lagrange_scaf "algebra/" )"finite_group[T, *, one]" p_groups nil )nil lagrange_scaf "algebra/" )nil finite_sets nil )"R" extend nil )"bool" sets nil )"{X: set[T] | subset?(X, G)}" normalizer_centralizernil )nil monad "algebra/" )nil group "algebra/" )nil monad "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )"bool" sets nil )nil general_properties nil )"bool" divides nil )"nat" p_groups nil )"{S: set[T] | subset?(S, G)}" nil )"{x: (G!1) | NOT member(x, center(G!1))}" nil )nil normalizer_centralizernil )"(partial_order?[set[T]])" nil )nil finite_sets nil )nil number_fields nil )nil number_fields nil )"bool" monad_def "algebra/" )nil monad "algebra/" )nil lagrange_index nil )"(CLs_nc(G!1))" p_groups nil )nil divides nil )nil normalizer_centralizer nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"R" restrict nil )"real" sigma_set "sigma_set/" )"bool" convergence_set "sigma_set/" )nil finite_sets nil )"bool" finite_sets nil )"nat" p_groups nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" p_groups nil )nil p_groups nil )"posnat" monad "algebra/" )nil group "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )"set" sets nil )nil groups_scaf nil )"real" reals nil )"int" integers nil )nil integers nil )nil general_properties nil )nil general_properties nil )nil normalizer_centralizer nil )nil group_action nil )nil normalizer_centralizer nil )nil group "algebra/" )nil group_action nil )"bool" group_def "algebra/" )nil group "algebra/" )"(G)" normalizer_centralizer nil )nil class_equation_scaf nil )nil normalizer_centralizer nil )"setofsets[T]" normalizer_centralizer nil )"T" p_groups nil )nil primes "ints/" )nil exponentiation nil )nil exponentiation nil )"(total_order?[real])" nil )"posint" exponentiation nil )nil real_types nil )nil real_types nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" sets nil )"{s: set[T] | subset?(s, G)}" group "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T" p_groups nil )"[T, T -> T]" p_groups nil )set type-eq-decl nil sets nil )nil p_groups 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 3530273648 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3530396563"" (skosimp*)"" (lemma "Lagrange" )"" (inst -1 "G!1" "center(G!1)" )"1" (prop)"1" (replace -3 -1)"1" (lemma "divides_prime_power" )"1" (inst -1 "2" "p!1" "order(center(G!1))" )"1" (assert )"1" (skosimp)"1" (hide -3)"1" (case-replace "i!1 = 0" :hide? T)"1" (hide -1)"1" (rewrite "expt_x0" )"1" (lemma "prime_gt_1" )"1" "1" assert )"1" "burside_theorem" )"1" "p!1" "G!1" )"1" "1" "1" (assert ) nil nil ))nil )"2" "2" "2" "expt_ge1" )"2" "2" expand * ">=" ">" )"2" expand "<=" )"2" assert )"2" "2" "2" replace "2" "2" "both_sides_expt_gt1_lt" )"2" "p!1" "2" "1" )"2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "p_group_iff_power" )"3" "3" assert )"3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "i!1 = 1" :hide? T)"1" (rewrite "expt_x1" )"1" (hide 1)"1" "order_factor" )"1" "G!1" "center(G!1)" )"1" "1" "card_extend[set[T], left_cosets[T, *, one](G!1,center(G!1))]" )"1" "1" "1" "1" "1" "exponentiation.expt_div" )"1" "2" "1" "p!1" )"1" rewrite "expt_x1" )"1" "1" "prime_order_cycle[left_cosets(G!1,center(G!1)),mult(G!1,center(G!1)),center(G!1)]" )"1" "1" expand "order" )"1" assert )"1" "1" rewrite "factor_cyclic" )nil nil ))nil ))nil ))nil )"2" "2" expand "finite_group?" )"2" "card_factor_TCC1" )"2" "2" assert )"2" "1" expand "/" )"1" rewrite "finite_extension[set[T],left_cosets[T, *, one](G!1, center[T, *, one](G!1))]" )nil nil ))nil )"2" "2" rewrite "center_is_normal[T, *, one]" )"2" "2" rewrite "fullset_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "center(G!1)" )"2" "one" )"1" rewrite "left_coset_one" )nil nil )"2" rewrite "one_in" )nil nil ))nil ))nil ))nil )"3" "3" rewrite "left_cosets_group" )"3" "3" "center_is_normal[T, *, one]" )"1" "1" assert )"1" expand "normal_subgroup?" )"1" "1" "1" expand "subgroup?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "fullset_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "one" )"1" rewrite "left_coset_one" )nil nil )"2" rewrite "one_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "card_factor_TCC1" )"2" "2" assert )"2" "1" rewrite "finite_extension[set[T],left_cosets[T, *, one](G!1, center[T, *, one](G!1))]" )nil nil )"2" "2" rewrite "center_is_normal[T, *, one]" )"2" "2" rewrite "fullset_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "center_is_normal[T, *, one]" )"2" "2" rewrite "fullset_is_group" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "G!1" )"2" "finite_subgroups" )"2" "center(G!1)" "G!1" )"2" assert )"2" "2" rewrite "center_subgroup" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "<=" )"2" (assert )"2" "2" "2" expand "order" )"2" replace -1 -2 rl)"2" "2" "same_card_subset[T]" )"2" "center(G!1)" "G!1" )"2" assert )"2" "2" "abelian_eq_center[T,*,one]" )"1" "1" assert )nil nil ))nil )"2" "2" rewrite "fullset_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 )"2" (hide (-1 -2 2))"2" (rewrite "center_subgroup" ) nil nil )) nil ))nil )"2" (hide (-1 -2 2))"2" (lemma "finite_subgroups" )"2" (inst -1 "center(G!1)" "G!1" )"2" (assert )"2" (hide 2)"2" (lemma "center_subgroup" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" p_groups nil )"[T, T -> T]" p_groups nil )nil p_groups nil )nil lagrange "algebra/" )nil general_properties nil )"posint" exponentiation nil )nil extend_set_props nil )"set[T]" cosets "algebra/" )nil cosets "algebra/" )nil reals nil )"boolean" notequal nil )nil factor_groups "algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil cosets "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )"(total_order?[real])" nil )nil p_groups nil )"setofsets[T]" right_left_cosets nil )nil sets nil )nil group "algebra/" )"bool" group_def "algebra/" )"R" restrict nil )nil defined_types nil )nil extend_set_props nil )nil groups_scaf nil )nil p_groups nil )nil right_left_cosets nil )"bool" booleans nil )"set" sets nil )nil finite_cyclic_groups"algebra/" )nil exponentiation nil )nil finite_sets nil )"group[left_cosets(G, N), mult(G, N), N]" nil )"left_cosets(G, H)" factor_groups "algebra/" )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )"bool" finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )nil group "algebra/" )nil lagrange_index nil )nil finite_sets nil )"(partial_order?[set[T]])" nil )nil groups_scaf nil )nil primes "ints/" )nil p_groups nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil exponentiation nil )nil exponentiation nil )"bool" reals nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil p_groups nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )"posnat" monad "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers 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 booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"bool" sets nil )"{s: set[T] | subset?(s, G)}" group "algebra/" )nil group "algebra/" )"finite_group[T, *, one]" p_groups nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.138 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
