|
%------------------------------------------------------------------------------
% Abelian Groups
%
% Author: David Lester, Manchester University & NIA
% Rick Butler
%
% Version 1.0 3/1/02
% Version 1.1 12/3/03 New library structure
% Version 1.2 5/5/04 Reworked for definition files DRL
%------------------------------------------------------------------------------
abelian_group[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_abelian_group: ASSUMPTION abelian_group?(fullset[T])
ENDASSUMING
IMPORTING monoid_def, group_def,
group[T,*,one]
abelian_group: NONEMPTY_TYPE = (abelian_group?) CONTAINING fullset[T]
A: VAR abelian_group
S: VAR set[T]
abelian_group_is_group: JUDGEMENT abelian_group SUBTYPE_OF group
abelian_group_is_commutative_monoid:
JUDGEMENT abelian_group SUBTYPE_OF commutative_monoid
abelian_subgroups: LEMMA subgroup?(S,A) IMPLIES abelian_group?(S)
finite_abelian_group: TYPE+ = (finite_abelian_group?)
G: VAR finite_abelian_group
finite_abelian_group_is_abelian_group:
JUDGEMENT finite_abelian_group SUBTYPE_OF abelian_group
finite_abelian_group_is_finite_group:
JUDGEMENT finite_abelian_group SUBTYPE_OF finite_group
finite_abelian_subgroups:
LEMMA subgroup?(S,G) IMPLIES finite_abelian_group?(S)
END abelian_group
¤ Dauer der Verarbeitung: 0.1 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.
|
