Quelle  lagrange_index.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