|
cyclic_group[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
%------------------------------------------------------------------------
% The imported type T with * and one must be a group.
% From this foundation other groups are created. These are just subgroups of the
% underlying imported type.
%------------------------------------------------------------------------
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING group[T,*,one]
a: VAR T
S: VAR set[T]
H,G: VAR group
i: VAR int
% generated_by(a): group = {t: T | EXISTS (i: int): t = a^i}
% cyclic?(G): boolean = EXISTS (a:(G)): G = generated_by(a)
generated_by_lem : LEMMA generated_by(a)(a^i)
generated_is_subgroup: LEMMA member(a,G) IMPLIES
subgroup?(generated_by(a),G)
generated_by_is_finite: LEMMA S = generated_by(a) AND
(EXISTS (k: posnat): a^k = one)
IMPLIES finite_group?(S)
cyclic_abelian: THEOREM cyclic?(G) IMPLIES abelian_group?(G)
%% TRICKY %%
cyclic_subgroup: LEMMA subgroup?(H,G) AND cyclic?(G) IMPLIES cyclic?(H)
is_cyclic : LEMMA (EXISTS (a:(G)): FORALL (x: (G)):
EXISTS (n: nat): x = a^n) IMPLIES
cyclic?(G)
END cyclic_group
¤ 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.
|
