Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 4 kB

Quelle sylow_theorems.pvs Sprache: PVS

%%-------------------** Sylow Theorems **-------------------
%%
%% Author          : André Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------

sylow_theorems[T: TYPE, *: [T,T -> T], one: T]: THEORY

BEGIN

   ASSUMING IMPORTING algebra@group_def

       T_is_group: ASSUMPTION group?[T,*,one](fullset[T])

   ENDASSUMING

   IMPORTING algebra@finite_groups[T,*,one],
             isomorphism_theorems,
             p_groups

             G: VAR group[T,*,one]
             X: VAR setofsets[T]
    p, n, m, i: VAR posnat

%%%%% Definitions %%%%%

   p_subgroup_sylow?(G:finite_group, p:{p: posnat | prime?(p)})(P:subgroup(G)): bool =
      p_group?[T,*,one](P,p) AND
     (FORALL (H: subgroup(G)): p_group?[T,*,one](H,p) AND subgroup?(P,H) IMPLIES P = H)

   p_subgroup_sylow(G:finite_group, p:{p: posnat | prime?(p)}): setofsets[T] =
                                                                {P: subgroup(G) | p_subgroup_sylow?(G,p)(P)}

   is_conjugate(G:finite_group,H:subgroup(G))(S:subgroup(G)): bool = EXISTS (a: (G)): S = a*H*inv(a)

   action_by_c(G:finite_group, X)(a:(G), P:(X)): set[T] = a*P*inv(a)

%%%%% Quotient subgroups %%%%%

   subgroup_is_factor: LEMMA FORALL (N: normal_subgroup(G), S: subgroup(G/N)):
                                      EXISTS (H: subgroup(G)): subgroup?(N,H) AND S = H/N

%%%%% First Sylow Theorem %%%%%

   First_Sylow_Theorem: THEOREM
            FORALL (G:finite_group): prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND i <= n
               IMPLIES
                     (EXISTS (H: subgroup(G)): order(H) = p^i)
                                      AND
                     (FORALL (S: subgroup(G)): order(S) = p^(i - 1)
                        IMPLIES
                           EXISTS (K: subgroup(G)): order(K) = p^i AND normal_subgroup?(S,K))

   p_group_is_subgroup: COROLLARY
               FORALL (G:finite_group, H: subgroup(G)):
                 prime?(p) AND gcd(p,m) = 1 AND i <= n AND order(G) = p^(n)*m  AND order(H) = p^(n - i)
                  IMPLIES
                     EXISTS (K: subgroup(G)): order(K) = p^(n) AND subgroup?(H,K)

   p_subgroup_sylow_order: COROLLARY FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1
                                            IMPLIES
                                                (p_subgroup_sylow?(G,p)(P) IFF order(P) = p^(n))

   conjugate_is_p_subgroup_sylow: COROLLARY  FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
                                        p_subgroup_sylow?(G,p)(P)
                                            IMPLIES
                                                FORALL (a:(G)): p_subgroup_sylow?(G,p)(a*P*inv(a))

   unique_is_normal: COROLLARY  FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
                                        p_subgroup_sylow(G,p) = singleton(P)
                                            IMPLIES
                                                normal_subgroup?(P,G)

%%%%% Second Sylow Theorem %%%%%

   Second_Sylow_Theorem: THEOREM
            FORALL (G:finite_group, P, K:subgroup(G)):
               prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
               p_subgroup_sylow?(G,p)(P) AND p_group?[T,*,one](K,p)
                  IMPLIES
                     EXISTS (a:(G)): subgroup?(K,a*P*inv(a))
                                      AND
                     (p_subgroup_sylow?(G,p)(K) IMPLIES is_conjugate(G,P)(K))

%%%%% Third Sylow Theorem %%%%%

   Third_Sylow_Theorem: THEOREM
            FORALL (G:finite_group, P:subgroup(G)):
               prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
               p_subgroup_sylow?(G,p)(P)
                   IMPLIES
                     LET np = card(p_subgroup_sylow(G,p)) IN
                     np = index(G, normalizer(G,P)) AND divides(np,m) AND divides(p, np -1)

END sylow_theorems

quality92%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.