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 (* $Id: CVectorSpace.v,v 1.4 2004/04/23 10:00:54 lcf Exp $ *)
21 (*#* printing ['] %{'}% #'# *)
23 include "algebra/CFields.ma".
28 Obsolete but maintained.
34 Set Implicit Arguments.
38 Unset Strict Implicit.
43 inline procedural "cic:/CoRN/algebra/CVectorSpace/VSpace.ind".
46 cic:/matita/CoRN-Procedural/algebra/CVectorSpace/vs_vs.con
56 Unset Implicit Arguments.
62 Hint Resolve vs_assoc vs_unit vs_distl vs_distr: algebra.
66 Implicit Arguments vs_op [F v].
70 Infix "[']" := vs_op (at level 30, no associativity).
75 Let [F] be a fiels and let [V] be a vector space over [F]
84 cic:/CoRN/algebra/CVectorSpace/VS_basics/F.var
88 cic:/CoRN/algebra/CVectorSpace/VS_basics/V.var
91 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_zero.con" as lemma.
93 inline procedural "cic:/CoRN/algebra/CVectorSpace/zero_vs_op.con" as lemma.
96 Hint Resolve vs_op_zero zero_vs_op: algebra.
99 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_inv_V.con" as lemma.
101 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_inv_S.con" as lemma.
104 Hint Resolve vs_op_inv_V vs_op_inv_S: algebra.
107 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_inv_assoc.con" as lemma.
110 Hint Resolve vs_inv_assoc: algebra.
113 inline procedural "cic:/CoRN/algebra/CVectorSpace/ap_zero_vs_op_l.con" as lemma.
115 inline procedural "cic:/CoRN/algebra/CVectorSpace/ap_zero_vs_op_r.con" as lemma.
117 (* note this is the same proof as mult_resp_ap_zero *)
119 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_rht.con" as lemma.
121 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_zero.con" as lemma.
123 inline procedural "cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_lft.con" as lemma.
130 Hint Resolve vs_op_zero zero_vs_op: algebra.