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/monoids/".
17 include "algebra/semigroups.ma".
19 record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝
20 { e_is_left_unit: is_left_unit SS e;
21 e_is_right_unit: is_right_unit SS e
24 record Monoid : Type ≝
25 { semigroup: SemiGroup;
27 properties: isMonoid ? e
30 coercion cic:/matita/algebra/monoids/semigroup.con.
32 definition is_left_inverse ≝
33 λM:Monoid. let op ≝ op M in let e ≝ e M in
35 ∀x:M. op (opp x) x = e.
37 definition is_right_inverse ≝
38 λM:Monoid. let op ≝ op M in let e ≝ e M in
40 ∀x:M. op x (opp x) = e.
42 theorem is_left_inverse_to_is_right_inverse_to_eq:
43 ∀M:Monoid. ∀oppL,oppR.
44 is_left_inverse M oppL → is_right_inverse M oppR →
45 ∀x:M. oppL x = oppR x.
49 generalize in match (H x); intro;
50 change in H2 with (op (oppL x) x = e);
51 generalize in match (eq_f ? ? (λy. op y (oppR x)) ? ? H2);
52 simplify; fold simplify op;
54 generalize in match (properties (semigroup M)); intro;
55 unfold isSemiGroup in H2; unfold associative in H2;
56 rewrite > H2 in H3; clear H2;
58 rewrite > (e_is_left_unit ? ? (properties M)) in H3;
59 rewrite > (e_is_right_unit ? ? (properties M)) in H3;