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 notation "hvbox(! \sub S)"
35 interpretation "Monoid unit" 'munit S =
36 (cic:/matita/algebra/monoids/e.con S).
38 definition is_left_inverse ≝
41 ∀x:M. op M (opp x) x = ! \sub M.
43 definition is_right_inverse ≝
46 ∀x:M. op M x (opp x) = ! \sub M.
48 theorem is_left_inverse_to_is_right_inverse_to_eq:
49 ∀M:Monoid. ∀oppL,oppR.
50 is_left_inverse M oppL → is_right_inverse M oppR →
51 ∀x:M. oppL x = oppR x.
53 generalize in match (H x); intro;
54 generalize in match (eq_f ? ? (λy. op M y (oppR x)) ? ? H2);
55 simplify; fold simplify (op M);
57 generalize in match (properties (semigroup M));
58 fold simplify (Type_of_Monoid M);
60 unfold isSemiGroup in H2; unfold associative in H2;
61 rewrite > H2 in H3; clear H2;
63 rewrite > (e_is_left_unit ? ? (properties M)) in H3;
64 rewrite > (e_is_right_unit ? ? (properties M)) in H3;