|
finite_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
% Cyclic Groups
%
% Author: Rick Butler and David Lester
%
% 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 group[T,*,one],
ints@primes
G,H: VAR finite_group
S: VAR (nonempty?[T])
a,b: VAR T
n: VAR nat
finite_generated_by: LEMMA member(a,G) IMPLIES
is_finite(generated_by(a)) %% RWB
finite_generated_by_def: LEMMA member(a,G) AND S = generated_by(a)
IMPLIES S = {t:T | EXISTS (n:posnat): n <= card(S) AND t = a^n}
finite_generated_by_one: LEMMA member(a,G) AND S = generated_by(a)
IMPLIES a^card(S) = one
generated_by_card_1: LEMMA member(a,G) AND
card(generated_by(a)) = 1
IMPLIES a = one AND
generated_by(a) = singleton[T](one)
finite_group_elements: LEMMA member(a,G) IMPLIES finite_order?(a)
period(G:finite_group,a:(G)):posnat = min({n:posnat | a^n = one})
a_hat_period: LEMMA member(a,G) IMPLIES a^(period(G,a)) = one
finite_subgroup_def: LEMMA
subgroup?(S,G) IFF (subset?(S,G) AND star_closed?(S))
orders_equal: LEMMA order(H) = order(G) AND subgroup?(H,G)
IMPLIES G = H
IMPORTING lagrange[T,*,one]
period_is_generated_order: LEMMA member(a,G) IMPLIES
period(G,a) = order(generated_by(a))
period_element_divides_group: COROLLARY member(a,G) IMPLIES
divides(period(G,a),order(G))
END finite_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.
|
