%%-------------------** Zn Group **-------------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------
zp_group[n:posnat]: THEORY
BEGIN
IMPORTING algebra@group
Zn: set[below(n)] = {m: nat | m < n};
++(a,b: below(n)): below(n) = rem(n)(a+b)
Zn_group: LEMMA group?[below(n), ++, 0](Zn)
Zn_finite: LEMMA is_finite(Zn)
Zn_card: LEMMA card(Zn) = n
END zp_group
¤ Dauer der Verarbeitung: 0.12 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.
|