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/CFields".
19 (* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *)
21 (*#* printing [/] %\ensuremath{/}% #/# *)
23 (*#* printing [//] %\ensuremath\ddagger% #‡# *)
25 (*#* printing {/} %\ensuremath{/}% #/# *)
27 (*#* printing {1/} %\ensuremath{\frac1\cdot}% #1/# *)
29 (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *)
100 Transparent cg_minus.
115 (* Begin_SpecReals *)
120 * Fields %\label{section:fields}%
121 ** Definition of the notion Field
124 inline cic:/CoRN/algebra/CFields/is_CField.con.
126 inline cic:/CoRN/algebra/CFields/CField.ind.
130 inline cic:/CoRN/algebra/CFields/f_rcpcl'.con.
132 inline cic:/CoRN/algebra/CFields/f_rcpcl.con.
135 Implicit Arguments f_rcpcl [F].
139 [cf_div] is the division in a field. It is defined in terms of
140 multiplication and the reciprocal. [x[/]y] is only defined if
141 we have a proof of [y [#] Zero].
144 inline cic:/CoRN/algebra/CFields/cf_div.con.
147 Implicit Arguments cf_div [F].
151 %\begin{convention}\label{convention:div-form}%
152 - Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].
153 - In lemmas, a hypothesis that [t [#] Zero] will be named [t_].
154 - We do not use [NonZeros], but write the condition [ [#] Zero] separately.
155 - In each lemma, we use only variables for proof objects, and these variables
156 are universally quantified.
157 For example, the informal lemma
158 $\frac{1}{x}\cdot\frac{1}{y} = \frac{1}{x\cdot y}$
159 #(1/x).(1/y) = 1/(x.y)# for all [x] and [y]is formalized as
161 forall (x y : F) x_ y_ xy_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//]xy_
165 forall (x y : F) x_ y_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//](prod_nz x y x_ y_)
167 We have made this choice to make it easier to apply lemmas; this can
168 be quite awkward if we would use the last formulation.
169 - So every division occurring in the formulation of a lemma is of the
170 form [e[/]e'[//]H] where [H] is a variable. Only exceptions: we may
171 write [e[/] (Snring n)] and [e[/]TwoNZ], [e[/]ThreeNZ] and so on.
172 (Constants like [TwoNZ] will be defined later on.)
177 %\begin{convention}% Let [F] be a field.
182 Section Field_axioms.
185 inline cic:/CoRN/algebra/CFields/F.var.
187 inline cic:/CoRN/algebra/CFields/CField_is_CField.con.
189 inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con.
196 Section Field_basics.
200 %\begin{convention}% Let [F] be a field.
204 inline cic:/CoRN/algebra/CFields/F.var.
206 inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con.
208 inline cic:/CoRN/algebra/CFields/field_mult_inv.con.
211 Hint Resolve field_mult_inv: algebra.
214 inline cic:/CoRN/algebra/CFields/field_mult_inv_op.con.
221 Hint Resolve field_mult_inv field_mult_inv_op: algebra.
225 Section Field_multiplication.
229 ** Properties of multiplication
230 %\begin{convention}% Let [F] be a field.
234 inline cic:/CoRN/algebra/CFields/F.var.
236 inline cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con.
238 inline cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con.
240 inline cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con.
242 inline cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con.
244 inline cic:/CoRN/algebra/CFields/mult_resp_neq.con.
246 inline cic:/CoRN/algebra/CFields/mult_eq_zero.con.
248 inline cic:/CoRN/algebra/CFields/mult_cancel_lft.con.
250 inline cic:/CoRN/algebra/CFields/mult_cancel_rht.con.
252 inline cic:/CoRN/algebra/CFields/square_eq_aux.con.
254 inline cic:/CoRN/algebra/CFields/square_eq_weak.con.
256 inline cic:/CoRN/algebra/CFields/cond_square_eq.con.
259 End Field_multiplication.
266 inline cic:/CoRN/algebra/CFields/x_xminone.con.
268 inline cic:/CoRN/algebra/CFields/square_id.con.
275 Hint Resolve mult_resp_ap_zero: algebra.
279 Section Rcpcl_properties.
283 ** Properties of reciprocal
284 %\begin{convention}% Let [F] be a field.
288 inline cic:/CoRN/algebra/CFields/F.var.
290 inline cic:/CoRN/algebra/CFields/inv_one.con.
292 inline cic:/CoRN/algebra/CFields/f_rcpcl_wd.con.
294 inline cic:/CoRN/algebra/CFields/f_rcpcl_mult.con.
296 inline cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con.
298 inline cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con.
301 End Rcpcl_properties.
309 ** The multiplicative group of nonzeros of a field.
310 %\begin{convention}% Let [F] be a field
314 inline cic:/CoRN/algebra/CFields/F.var.
317 The multiplicative monoid of NonZeros.
320 inline cic:/CoRN/algebra/CFields/NonZeroMonoid.con.
322 inline cic:/CoRN/algebra/CFields/fmg_cs_inv.con.
324 inline cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con.
326 inline cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con.
333 Section Div_properties.
337 ** Properties of division
338 %\begin{convention}% Let [F] be a field.
341 %\begin{nameconvention}%
342 In the names of lemmas, we denote [[/]] by [div], and
344 %\end{nameconvention}%
347 inline cic:/CoRN/algebra/CFields/F.var.
349 inline cic:/CoRN/algebra/CFields/div_prop.con.
351 inline cic:/CoRN/algebra/CFields/div_1.con.
353 inline cic:/CoRN/algebra/CFields/div_1'.con.
355 inline cic:/CoRN/algebra/CFields/div_1''.con.
358 Hint Resolve div_1: algebra.
361 inline cic:/CoRN/algebra/CFields/x_div_x.con.
364 Hint Resolve x_div_x: algebra.
367 inline cic:/CoRN/algebra/CFields/x_div_one.con.
370 The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$
374 inline cic:/CoRN/algebra/CFields/x_mult_y_div_z.con.
377 Hint Resolve x_mult_y_div_z: algebra.
380 inline cic:/CoRN/algebra/CFields/div_wd.con.
383 Hint Resolve div_wd: algebra_c.
387 The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$
388 #[(x/y)/z = x/(y.z)]#
391 inline cic:/CoRN/algebra/CFields/div_div.con.
393 inline cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con.
395 inline cic:/CoRN/algebra/CFields/div_resp_ap_zero.con.
398 The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$
399 #[x/(y/z) = (x.z)/y]#
402 inline cic:/CoRN/algebra/CFields/div_div2.con.
405 The next lemma says $\frac{x\cdot p}{y\cdot q} = \frac{x}{y}\cdot \frac{p}{q}$
406 #[(x.p)/(y.q) = (x/y).(p/q)]#
409 inline cic:/CoRN/algebra/CFields/mult_of_divs.con.
411 inline cic:/CoRN/algebra/CFields/div_dist.con.
413 inline cic:/CoRN/algebra/CFields/div_dist'.con.
415 inline cic:/CoRN/algebra/CFields/div_semi_sym.con.
418 Hint Resolve div_semi_sym: algebra.
421 inline cic:/CoRN/algebra/CFields/eq_div.con.
423 inline cic:/CoRN/algebra/CFields/div_strext.con.
430 Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2
431 mult_of_divs x_mult_y_div_z mult_of_divs div_dist div_dist' div_semi_sym
436 ** Cancellation laws for apartness and multiplication
437 %\begin{convention}% Let [F] be a field
442 Section Mult_Cancel_Ap_Zero.
445 inline cic:/CoRN/algebra/CFields/F.var.
447 inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con.
449 inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con.
451 inline cic:/CoRN/algebra/CFields/recip_ap_zero.con.
453 inline cic:/CoRN/algebra/CFields/recip_resp_ap.con.
456 End Mult_Cancel_Ap_Zero.
464 ** Functional Operations
466 We now move on to lifting these operations to functions. As we are
467 dealing with %\emph{partial}% #<i>partial</i># functions, we don't
468 have to worry explicitly about the function by which we are dividing
469 being non-zero everywhere; this will simply be encoded in its domain.
472 Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively
477 inline cic:/CoRN/algebra/CFields/X.var.
479 inline cic:/CoRN/algebra/CFields/F.var.
481 inline cic:/CoRN/algebra/CFields/G.var.
485 inline cic:/CoRN/algebra/CFields/P.con.
487 inline cic:/CoRN/algebra/CFields/Q.con.
492 Section Part_Function_Recip.
496 Some auxiliary notions are helpful in defining the domain.
499 inline cic:/CoRN/algebra/CFields/R.con.
501 inline cic:/CoRN/algebra/CFields/Ext2R.con.
503 inline cic:/CoRN/algebra/CFields/part_function_recip_strext.con.
505 inline cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con.
507 inline cic:/CoRN/algebra/CFields/Frecip.con.
510 End Part_Function_Recip.
514 Section Part_Function_Div.
518 For division things work out almost in the same way.
521 inline cic:/CoRN/algebra/CFields/R.con.
523 inline cic:/CoRN/algebra/CFields/Ext2R.con.
525 inline cic:/CoRN/algebra/CFields/part_function_div_strext.con.
527 inline cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con.
529 inline cic:/CoRN/algebra/CFields/Fdiv.con.
532 End Part_Function_Div.
536 %\begin{convention}% Let [R:X->CProp].
540 inline cic:/CoRN/algebra/CFields/R.var.
542 inline cic:/CoRN/algebra/CFields/included_FRecip.con.
544 inline cic:/CoRN/algebra/CFields/included_FRecip'.con.
546 inline cic:/CoRN/algebra/CFields/included_FDiv.con.
548 inline cic:/CoRN/algebra/CFields/included_FDiv'.con.
550 inline cic:/CoRN/algebra/CFields/included_FDiv''.con.
557 Implicit Arguments Frecip [X].
561 Implicit Arguments Fdiv [X].
565 Hint Resolve included_FRecip included_FDiv : included.
569 Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included.