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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbMonoids".
24 Section Abelian_Monoids.
29 Now we introduce commutativity and add some results.
32 inline cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con.
34 inline cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind.
37 Section AbMonoid_Axioms.
40 inline cic:/CoRN/algebra/CAbMonoids/M.var.
43 %\begin{convention}% Let [M] be an abelian monoid.
47 inline cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con.
49 inline cic:/CoRN/algebra/CAbMonoids/cam_commutes.con.
51 inline cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con.
58 Section SubCAbMonoids.
62 ** Subgroups of an Abelian Monoid
65 inline cic:/CoRN/algebra/CAbMonoids/M.var.
67 inline cic:/CoRN/algebra/CAbMonoids/P.var.
69 inline cic:/CoRN/algebra/CAbMonoids/Punit.var.
71 inline cic:/CoRN/algebra/CAbMonoids/op_pres_P.var.
75 Let [M] be an Abelian Monoid and [P] be a ([CProp]-valued) predicate on [M]
76 that contains [Zero] and is closed under [[+]] and [[--]].
80 inline cic:/CoRN/algebra/CAbMonoids/subcrr.con.
82 inline cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con.
84 inline cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con.
95 Hint Resolve cam_commutes_unfolded: algebra.