|
%%-------------------** Some properties of groups and subgroups **-------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%------------------------------------------------------------------------------
groups_scaf[T: TYPE, *: [T,T -> T], one: T]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING algebra@group,
algebra@factor_groups,
algebra@finite_groups[T,*,one],
general_properties,
right_left_cosets
G, H, N, K: VAR group
a, b, c: VAR T
p, k: VAR posnat
m: VAR int
i: VAR nat
%%%%% Definitions %%%%%
subgroup_contain(G: group, N: subgroup(G)): TYPE = {H: group | subgroup?(H,G) AND subset?(N, H)}
%%%%% Properties of groups and subgroups %%%%%
divby_r: LEMMA a = b * c IFF a * inv[T,*,one](c) = b
subgroup_transitive: LEMMA subgroup?(H,G) AND subgroup?(K,H)
IMPLIES subgroup?(K,G)
normal_subgroup_tran: LEMMA subgroup?(H,G) AND subgroup?(N,H) AND
normal_subgroup?(N,G)
IMPLIES normal_subgroup?(N,H)
subgroup_intersection: LEMMA subgroup?(H,G) AND subgroup?(K,G)
IMPLIES subgroup?(intersection(H,K),G)
conjugate_is_subgroup: LEMMA FORALL (a: (G), H:subgroup(G)): subgroup?(a*H*inv(a),G)
center_is_normal: LEMMA normal_subgroup?(center(G),G)
abelian_eq_center: LEMMA abelian_group?(G) IFF G = center(G)
order_gt_1: LEMMA FORALL (G:finite_group):
prime?(p) AND divides(p, order(G)) IMPLIES order(G) > 1
order_gt_p: LEMMA FORALL (G:finite_group):
prime?(p) AND divides(p, order(G)) IMPLIES order(G) >= p
exists_diff_one: LEMMA FORALL (G:finite_group):
order(G) > 1 IMPLIES EXISTS (x: (G)): x /= one
one_iff_divides: LEMMA FORALL (G:finite_group, a:(G)):
a^m = one IFF divides(period(G,a), m)
order_power: LEMMA FORALL (G:finite_group, a:(G)):
LET n = period(G,a) IN
period(G,a^k) = n / gcd(k,n)
coset_power_nat: LEMMA FORALL (x:(G), H:normal_subgroup(G)):
^[left_cosets(G,H),mult(G,H),H](x*H, i) = (x^i)*H
coset_power_int: LEMMA FORALL (x:(G), H:normal_subgroup(G)):
^[left_cosets(G,H),mult(G,H),H](x*H, m) = (x^m)*H
END groups_scaf
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
