(lagrange_indexnil 3530436270"" (rewrite "fullset_is_group" ) nil nil )nil lagrange_index nil )) nil ))nil 3528627519"" (skosimp*)"" (expand * "order" "index" )"" (lemma "set_left_cosets_full" )"" (inst - "G!1" "H!1" )"" (lemma "card_eq_part[T]" )"" (inst?)"1" (assert )"1" (hide (-1 2))"1" (prop)"1" (skosimp)"1" (typepred "A!1" "B!1" )"1" (expand "left_cosets" )"1" (skosimp*)"1" "finite_left_coset_correspondence" )"1" "H!1" "a!1" "a!2" "G!1" )"1" assert )"1" expand "left_coset" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (lemma "left_cosets_disjoint" )"2" (inst - "G!1" "H!1" "A!1" "B!1" )"1" (assert ) nil nil )"2" (typepred "B!1" )"2" (expand "left_cosets" )"2" (propax) nil nil )) nil ))nil )"3" (typepred "A!1" )"3" (expand "left_cosets" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (expand "left_cosets" )"3" (inst + "one" )"1" (rewrite "left_coset_one" ) nil nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (lemma "left_cosets_partition" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" right_left_cosets nil )"posnat" monad "algebra/" )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/" )"finite_group[T, *, one]" lagrange_indexnil )"finite_group[T, *, one]" lagrange_indexnil )"setofsets[T]" right_left_cosets nil )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil lagrange_scaf "algebra/" )nil monad "algebra/" )"bool" monad_def "algebra/" )nil monad "algebra/" )nil cosets "algebra/" )"[T, T -> boolean]" equalities nil )"(left_cosets(G!1, H!1))" lagrange_indexnil )"set[T]" cosets "algebra/" )"(left_cosets(G!1, H!1))" lagrange_indexnil )nil cosets "algebra/" )nil right_left_cosets nil )nil nil )"bool" sets nil )"{s: set[T] | subset?(s, G)}" cosets"algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil right_left_cosets nil )nil lagrange_scaf "algebra/" )nil right_left_cosets nil )nil lagrange_index nil )"[T, T -> T]" lagrange_index nil )"T" lagrange_index nil ))nil 3530566927"" (skosimp*)"" (expand "divides" )"" (lemma "Lagrange_index" )"" (inst?) (("" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" divides nil )nil lagrange_index nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" lagrange_index nil )"T" lagrange_index nil )"bool" group_def "algebra/" )nil group "algebra/" )"posnat" monad "algebra/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil monad "algebra/" )"bool" monad_def "algebra/" )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 3530436270"" (skosimp*) (("" (rewrite "card_factor_TCC1" ) nil nil )) nil )nil right_left_cosets 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/" )nil lagrange_index nil )"[T, T -> T]" lagrange_index nil )"T" lagrange_index nil ))nil ))nil 3530436293"" (skosimp*)"" (lemma "card_factor" )"" (inst?)"" (assert )"" (replaces -1)"" (lemma "Lagrange_index" )"" (inst?)"" (assert )"" (expand "normal_subgroup?" )"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" lagrange_index nil )"[T, T -> T]" lagrange_index nil )nil lagrange_index nil )nil right_left_cosets nil )"posrat" nil )nil lagrange_index nil )"boolean" normal_subgroups "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 ))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
