|
%%-------------------** Lagrange Theorem **----------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------
lagrange_index[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING algebra@lagrange,
right_left_cosets[T,*,one],
algebra@normal_subgroups[T,*,one]
G,H,N: VAR finite_group
Lagrange_index: THEOREM subgroup?(H,G) IMPLIES order(G) = index(G, H) * order(H)
index_divides: COROLLARY subgroup?(H,G) IMPLIES divides(index(G, H), order(G))
order_factor: LEMMA normal_subgroup?(N, G) IMPLIES card[set[T]](G/N) = order(G)/order(N)
END lagrange_index
¤ Dauer der Verarbeitung: 0.16 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.
|
