| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
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 ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28