(**************************************************************************)
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(\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
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
- ∃e:G. isMonoid (mk_PreMonoid G e).
+ ∃e:G. IsMonoid (mk_PreMonoid G e).
intros;
letin f ≝(λn.ι(G \sub O · G \sub n));
cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
- rewrite > (op_associative ? G) in GOGO;
+ rewrite > (op_is_associative ? G) in GOGO;
letin GaGa ≝(H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
constructor 1;
[ simplify;
- apply (semigroup_properties G)
+ apply (is_semi_group G)
| unfold is_left_unit; intro;
letin GaxGax ≝(refl_eq ? (G \sub a ·x));
clearbody GaxGax; (* demo *)
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
+ rewrite > (op_is_associative ? G) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝(refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
+ rewrite < (op_is_associative ? G) in GaxGax;
apply (H1 ? ? ? GaxGax)
]
]