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/CVectorSpace".
19 (* $Id: CVectorSpace.v,v 1.4 2004/04/23 10:00:54 lcf Exp $ *)
21 (*#* printing ['] %{'}% #'# *)
30 Obsolete but maintained.
36 Set Implicit Arguments.
40 Unset Strict Implicit.
45 inline cic:/CoRN/algebra/CVectorSpace/VSpace.ind.
54 Unset Implicit Arguments.
60 Hint Resolve vs_assoc vs_unit vs_distl vs_distr: algebra.
64 Implicit Arguments vs_op [F v].
69 Let [F] be a fiels and let [V] be a vector space over [F]
77 inline cic:/CoRN/algebra/CVectorSpace/F.var.
79 inline cic:/CoRN/algebra/CVectorSpace/V.var.
81 inline cic:/CoRN/algebra/CVectorSpace/vs_op_zero.con.
83 inline cic:/CoRN/algebra/CVectorSpace/zero_vs_op.con.
86 Hint Resolve vs_op_zero zero_vs_op: algebra.
89 inline cic:/CoRN/algebra/CVectorSpace/vs_op_inv_V.con.
91 inline cic:/CoRN/algebra/CVectorSpace/vs_op_inv_S.con.
94 Hint Resolve vs_op_inv_V vs_op_inv_S: algebra.
97 inline cic:/CoRN/algebra/CVectorSpace/vs_inv_assoc.con.
100 Hint Resolve vs_inv_assoc: algebra.
103 inline cic:/CoRN/algebra/CVectorSpace/ap_zero_vs_op_l.con.
105 inline cic:/CoRN/algebra/CVectorSpace/ap_zero_vs_op_r.con.
107 (* note this is the same proof as mult_resp_ap_zero *)
109 inline cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_rht.con.
111 inline cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_zero.con.
113 inline cic:/CoRN/algebra/CVectorSpace/vs_op_resp_ap_lft.con.
120 Hint Resolve vs_op_zero zero_vs_op: algebra.