| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle lagrange_index.pvs Sprache: PVS |
|||||||||
|
%%-------------------** 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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28