Quelle lagrange.pvs Sprache: 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

quality99%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.