Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: lagrange.pvs Sprache: PVS

Original von: PVS^©

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

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.