| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle normal_subgroups.pvs Sprache: PVS |
|||||||||
|
normal_subgroups[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN ASSUMING IMPORTING group_def[T,*,one] fullset_is_group: ASSUMPTION group?(fullset[T]) ENDASSUMING IMPORTING cosets[T,*,one], ints@primes AUTO_REWRITE+ member inv(a:T): MACRO T = inv[T,*,one](a) H,G,N: VAR group[T,*,one] normal_prep: LEMMA (FORALL (a: (G)): subset?(inv(a)*N*a,N) ) AND subgroup?(N,G) IMPLIES FORALL (a: (G)): a*N*inv(a) = N normal_subgroup?(N: group[T,*,one], G: group[T,*,one]): boolean = subgroup?(N,G) AND FORALL (a: (G)): subset?(inv(a)*N*a,N) ; normal_left_is_right: THEOREM normal_subgroup?(N,G) IFF (subgroup?(N,G) AND (FORALL (a:(G)): a*N = N*a)) normal_subgroup(G): TYPE = {N: group | normal_subgroup?(N,G)} normal_subgroup_is_subgroup: JUDGEMENT normal_subgroup(G) SUBTYPE_OF subgroup(G) a,h: VAR T nsg_prop : LEMMA FORALL (G: group, H: normal_subgroup(G)): G(a) and H(h) IMPLIES H(a*h*inv(a)) nsg_prop2 : LEMMA FORALL (G: group, H: normal_subgroup(G)): G(a) and H(h) IMPLIES H(inv(a)*h*a) lc_gen_normal : LEMMA normal_subgroup?(H,G) AND G(a) IMPLIES (EXISTS (h: (H)): lc_gen(G,H,a*H) = h*a) abelian_normal: LEMMA abelian_group?(G) and subgroup?(H,G) IMPLIES normal_subgroup?(H,G) END normal_subgroups ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28