(**************************************************************************)
include "algebra/groups.ma".
+include "nat/relevant_equations.ma".
record finite_enumerable (T:Type) : Type≝
{ order: nat;
(* CSC: multiple interpretations in the same file are not considered in the
right order
-interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
+interpretation "Finite_enumerable representation" 'repr C i = (repr 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 _).
+interpretation "Finite_enumerable order" 'card C = (order C _).
record finite_enumerable_SemiGroup : Type≝
{ semigroup:> SemiGroup;
}.
interpretation "Finite_enumerable representation" 'repr S i =
- (cic:/matita/algebra/finite_groups/repr.con S
- (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
+ (repr S (is_finite_enumerable 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"
'index_of_finite_enumerable_semigroup e
=
- (cic:/matita/algebra/finite_groups/index_of.con _
- (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
+ (index_of _ (is_finite_enumerable _) e).
(* several definitions/theorems to be moved somewhere else *)
[ apply (H1 ? ? ? ? Hcut);
apply le_S;
assumption
- | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
-apply eq_pred_to_eq;
+ | apply eq_pred_to_eq;
[ apply (ltn_to_ltO ? ? H7)
| apply (ltn_to_ltO ? ? H6)
| assumption