|
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.0 Sekunden
(vorverarbeitet)
¤
|
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
