|
symmetric_groups[N: posnat]: THEORY
%
% RWB: adapted from old algebra library
%
BEGIN
S: set[posnat] = fullset[{n: posnat | n <= N}]
perm: TYPE = (bijective?[(S),(S)])
Sym: set[perm] = fullset[perm]
IMPORTING group_def
id: perm = identity[(S)]
op: [perm,perm -> perm] = function_props[(S),(S),(S)].o
Sym_is_group: LEMMA group?[perm,op,identity[(S)]](Sym)
% Sym_finite: LEMMA is_finite[perm](Sym) %% UNPROVED %%
% IMPORTING factorial
% order_Sym: LEMMA order[perm,op,id](Sym) = factorial(N) %% UNPROVED %%
END symmetric_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.
|
