| Quellcodebibliothek Statistik Leitseite 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 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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28