(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/algebra/finite_groups/".
-
include "algebra/groups.ma".
record finite_enumerable (T:Type) : Type≝
interpretation "Finite_enumerable representation" 'repr C i =
(cic:/matita/algebra/finite_groups/repr.con C _ i).*)
-notation < "hvbox(|C|)" with precedence 89
-for @{ 'card $C }.
-
interpretation "Finite_enumerable order" 'card C =
(cic:/matita/algebra/finite_groups/order.con C _).
(cic:/matita/algebra/finite_groups/repr.con S
(cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
-notation "hvbox(ι e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 60
for @{ 'index_of_finite_enumerable_semigroup $e }.
interpretation "Index_of_finite_enumerable representation"
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
assumption
]
| intros;
+ unfold f;
apply index_of_sur
]
].