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/CMonoids".
19 (* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *)
21 (*#* printing Zero %\ensuremath{\mathbf0}% #0# *)
30 * Monoids %\label{section:monoids}%
31 ** Definition of monoids
34 inline cic:/CoRN/algebra/CMonoids/is_rht_unit.con.
38 inline cic:/CoRN/algebra/CMonoids/is_lft_unit.con.
41 Implicit Arguments is_lft_unit [S].
47 Implicit Arguments is_rht_unit [S].
50 inline cic:/CoRN/algebra/CMonoids/is_CMonoid.ind.
52 inline cic:/CoRN/algebra/CMonoids/CMonoid.ind.
55 %\begin{nameconvention}%
56 In the names of lemmas, we will denote [Zero] with [zero].
57 We denote [ [#] Zero] in the names of lemmas by [ap_zero]
58 (and not, e.g.%\% [nonzero]).
59 %\end{nameconvention}%
65 The predicate "non-zero" is defined.
66 In lemmas we will continue to write [x [#] Zero], rather than
67 [(nonZeroP x)], but the predicate is useful for some high-level definitions,
68 e.g. for the setoid of non-zeros.
71 inline cic:/CoRN/algebra/CMonoids/nonZeroP.con.
76 Implicit Arguments nonZeroP [M].
81 %\begin{convention}% Let [M] be a monoid.
86 Section CMonoid_axioms.
89 inline cic:/CoRN/algebra/CMonoids/M.var.
91 inline cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con.
93 inline cic:/CoRN/algebra/CMonoids/cm_rht_unit.con.
95 inline cic:/CoRN/algebra/CMonoids/cm_lft_unit.con.
103 %\begin{convention}% Let [M] be a monoid.
108 Section CMonoid_basics.
111 inline cic:/CoRN/algebra/CMonoids/M.var.
113 inline cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con.
115 inline cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con.
118 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
121 inline cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con.
123 inline cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con.
125 (* Begin_SpecReals *)
128 The proof component of the monoid is irrelevant.
131 inline cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con.
138 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
146 inline cic:/CoRN/algebra/CMonoids/P.var.
148 inline cic:/CoRN/algebra/CMonoids/Punit.var.
150 inline cic:/CoRN/algebra/CMonoids/op_pres_P.var.
152 inline cic:/CoRN/algebra/CMonoids/subcrr.con.
154 inline cic:/CoRN/algebra/CMonoids/ismon_scrr.con.
156 inline cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con.
167 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.