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 (* This file was automatically generated: do not edit *********************)
19 include "algebra/CMonoids.ma".
22 Section Abelian_Monoids
27 Now we introduce commutativity and add some results.
30 inline procedural "cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con" as definition.
32 inline procedural "cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind".
35 cic:/matita/CoRN-Procedural/algebra/CAbMonoids/cam_crr.con
39 Section AbMonoid_Axioms
43 cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var
47 %\begin{convention}% Let [M] be an abelian monoid.
51 inline procedural "cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con" as lemma.
53 inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes.con" as lemma.
55 inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con" as lemma.
66 ** Subgroups of an Abelian Monoid
70 cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var
74 cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var
78 cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var
82 cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var
87 Let [M] be an Abelian Monoid and [P] be a ([CProp]-valued) predicate on [M]
88 that contains [Zero] and is closed under [[+]] and [[--]].
92 inline procedural "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/subcrr.con" "Abelian_Monoids__SubCAbMonoids__" as definition.
94 inline procedural "cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con" as lemma.
96 inline procedural "cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con" as definition.
107 Hint Resolve cam_commutes_unfolded: algebra.