%%-------------------** 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.1 Sekunden
(vorverarbeitet)
¤
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.