|
finite_cyclic_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
% Cyclic Groups
%
% Author: Rick Butler
%
% This are groups generated by an element and repeated multiplication
% using the following defined in theory group.
%
% generated_by(a): group = {t: T | EXISTS (i: int): t = a^i}
%
% cyclic?(G): boolean = EXISTS (a:(G)): G = generated_by(a)
%
%-----------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING finite_groups[T,*,one], cyclic_group[T,*,one],
ints@primes
G,H: VAR finite_group
S: VAR (nonempty?[T])
a,b: VAR T
n: VAR nat
prime_order_cycle: THEOREM prime?(order(G)) IMPLIES
cyclic?(G)
END finite_cyclic_groups
¤ 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.
|
