|
%------------------------------------------------------------------------------
% Lagrange
%
% Author: Rick Butler
% David Lester, Manchester University & NIA
%
% 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
%------------------------------------------------------------------------------
lagrange[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING group[T,*,one], cosets[T,*,one]
G,H: VAR finite_group
S: VAR (nonempty?[T])
a,b: VAR T
n: VAR nat
IMPORTING lagrange_scaf
% Herstein Lemma 2.4.5 (Corollary)
right_coset_finite: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
is_finite(right_coset(G,H)(a))
finite_right_coset_correspondence: LEMMA
subgroup?(H,G) AND member(a,G) AND member(b,G) IMPLIES
card(right_coset(G,H)(a)) = card(right_coset(G,H)(b))
% Herstein Theorem 2.4.1
set_right_cosets_full: LEMMA FORALL (G: group, H: subgroup(G)):
Union(fullset[right_cosets(G,H)]) = G
right_cosets_disjoint: LEMMA FORALL (G: group, H: subgroup(G), A,B: right_cosets(G, H)):
A = B OR disjoint?(A,B)
right_cosets_partition: LEMMA FORALL (G: finite_group, H: subgroup(G)):
finite_partition?[T](fullset[right_cosets(G, H)])
Lagrange: THEOREM subgroup?(H,G) IMPLIES divides(order(H),order(G)) %% NEW rwb
END lagrange
¤ Dauer der Verarbeitung: 0.15 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.
|
