X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;fp=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=a9164a927bde9cf2f937d77a2b8f0dabadd64428;hb=1561ac998b6823c9e763617fcb9cf3c063bb5e3b;hp=6eb0054c2fcb81fc93bd6c52cc5a70b5fe84d216;hpb=ff81867363f855a3ad5bba6f6bb636f20bf8a969;p=helm.git

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 6eb0054c2..a9164a927 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -14,3 +14,64 @@
 
 set "baseuri" "cic:/matita/algebra/groups/".
 
+include "algebra/monoids.ma".
+
+record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
+ { opp_is_left_inverse: is_left_inverse M opp;
+   opp_is_right_inverse: is_right_inverse M opp
+ }.
+ 
+record Group : Type ≝
+ { monoid: Monoid;
+   opp: monoid -> monoid;
+   group_properties: isGroup ? opp
+ }.
+ 
+coercion cic:/matita/algebra/groups/monoid.con.
+
+notation "hvbox(x \sup (-1))" with precedence 89
+for @{ 'gopp $x }.
+
+interpretation "Group inverse" 'gopp x =
+ (cic:/matita/algebra/groups/opp.con _ x).
+
+definition left_cancellable :=
+ \lambda T:Type. \lambda op: T -> T -> T.
+  \forall x,y,z. op x y = op x z -> y = z.
+  
+definition right_cancellable :=
+ \lambda T:Type. \lambda op: T -> T -> T.
+  \forall x,y,z. op y x = op z x -> y = z.
+  
+theorem eq_op_x_y_op_x_z_to_eq:
+ \forall G:Group. left_cancellable G (op G).
+intros;
+unfold left_cancellable;
+intros;
+rewrite < (e_is_left_unit ? ? (monoid_properties G));
+fold simplify (e G);
+rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
+fold simplify (e G);
+rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
+fold simplify (opp G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+apply eq_f;
+assumption.
+qed.
+
+(*
+theorem eq_op_x_y_op_z_y_to_eq:
+ \forall G:Group. right_cancellable G (op G).
+qed.
+
+definition has_cardinality :=
+ \lambda T:Type. \lambda n:nat.
+  \exists f. injective T nat f.
+
+definition finite :=
+ \lambda T:Type.
+  \exists f: T -> {n|n<
+*)