1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/groups/".
17 include "algebra/monoids.ma".
19 record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
20 { opp_is_left_inverse: is_left_inverse M opp;
21 opp_is_right_inverse: is_right_inverse M opp
26 opp: monoid -> monoid;
27 group_properties: isGroup ? opp
30 coercion cic:/matita/algebra/groups/monoid.con.
32 notation "hvbox(x \sup (-1))" with precedence 89
35 interpretation "Group inverse" 'gopp x =
36 (cic:/matita/algebra/groups/opp.con _ x).
38 definition left_cancellable :=
39 \lambda T:Type. \lambda op: T -> T -> T.
40 \forall x,y,z. op x y = op x z -> y = z.
42 definition right_cancellable :=
43 \lambda T:Type. \lambda op: T -> T -> T.
44 \forall x,y,z. op y x = op z x -> y = z.
46 theorem eq_op_x_y_op_x_z_to_eq:
47 \forall G:Group. left_cancellable G (op G).
49 unfold left_cancellable;
51 rewrite < (e_is_left_unit ? ? (monoid_properties G));
52 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
53 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
54 rewrite > (semigroup_properties G);
55 rewrite > (semigroup_properties G);
61 theorem eq_op_x_y_op_z_y_to_eq:
62 \forall G:Group. right_cancellable G (op G).
65 definition has_cardinality :=
66 \lambda T:Type. \lambda n:nat.
67 \exists f. injective T nat f.