matita/contribs/CoRN-Decl/algebra/CFields.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CFields".
  18
  19 (* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *)
  20
  21 (*#* printing [/] %\ensuremath{/}% #/# *)
  22
  23 (*#* printing [//] %\ensuremath\ddagger% #&Dagger;# *)
  24
  25 (*#* printing {/} %\ensuremath{/}% #/# *)
  26
  27 (*#* printing {1/} %\ensuremath{\frac1\cdot}% #1/# *)
  28
  29 (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?&Dagger;# *)
  30
  31 (* INCLUDE
  32 CRings
  33 *)
  34
  35 (* UNEXPORTED
  36 Transparent sym_eq.
  37 *)
  38
  39 (* UNEXPORTED
  40 Transparent f_equal.
  41 *)
  42
  43 (* UNEXPORTED
  44 Transparent cs_crr.
  45 *)
  46
  47 (* UNEXPORTED
  48 Transparent csg_crr.
  49 *)
  50
  51 (* UNEXPORTED
  52 Transparent cm_crr.
  53 *)
  54
  55 (* UNEXPORTED
  56 Transparent cg_crr.
  57 *)
  58
  59 (* UNEXPORTED
  60 Transparent cr_crr.
  61 *)
  62
  63 (* UNEXPORTED
  64 Transparent csf_fun.
  65 *)
  66
  67 (* UNEXPORTED
  68 Transparent csbf_fun.
  69 *)
  70
  71 (* UNEXPORTED
  72 Transparent csr_rel.
  73 *)
  74
  75 (* UNEXPORTED
  76 Transparent cs_eq.
  77 *)
  78
  79 (* UNEXPORTED
  80 Transparent cs_neq.
  81 *)
  82
  83 (* UNEXPORTED
  84 Transparent cs_ap.
  85 *)
  86
  87 (* UNEXPORTED
  88 Transparent cm_unit.
  89 *)
  90
  91 (* UNEXPORTED
  92 Transparent csg_op.
  93 *)
  94
  95 (* UNEXPORTED
  96 Transparent cg_inv.
  97 *)
  98
  99 (* UNEXPORTED
 100 Transparent cg_minus.
 101 *)
 102
 103 (* UNEXPORTED
 104 Transparent cr_one.
 105 *)
 106
 107 (* UNEXPORTED
 108 Transparent cr_mult.
 109 *)
 110
 111 (* UNEXPORTED
 112 Transparent nexp_op.
 113 *)
 114
 115 (* Begin_SpecReals *)
 116
 117 (* FIELDS *)
 118
 119 (*#*
 120 * Fields %\label{section:fields}%
 121 ** Definition of the notion Field
 122 *)
 123
 124 inline cic:/CoRN/algebra/CFields/is_CField.con.
 125
 126 inline cic:/CoRN/algebra/CFields/CField.ind.
 127
 128 (* End_SpecReals *)
 129
 130 inline cic:/CoRN/algebra/CFields/f_rcpcl'.con.
 131
 132 inline cic:/CoRN/algebra/CFields/f_rcpcl.con.
 133
 134 (* UNEXPORTED
 135 Implicit Arguments f_rcpcl [F].
 136 *)
 137
 138 (*#*
 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].
 142 *)
 143
 144 inline cic:/CoRN/algebra/CFields/cf_div.con.
 145
 146 (* UNEXPORTED
 147 Implicit Arguments cf_div [F].
 148 *)
 149
 150 (*#*
 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
 160 [[
 161 forall (x y : F) x_ y_ xy_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//]xy_
 162 ]]
 163 and not as
 164 [[
 165 forall (x y : F) x_ y_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//](prod_nz x y x_ y_)
 166 ]]
 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.)
 173
 174 %\end{convention}%
 175
 176 ** Field axioms
 177 %\begin{convention}% Let [F] be a field.
 178 %\end{convention}%
 179 *)
 180
 181 (* UNEXPORTED
 182 Section Field_axioms.
 183 *)
 184
 185 inline cic:/CoRN/algebra/CFields/F.var.
 186
 187 inline cic:/CoRN/algebra/CFields/CField_is_CField.con.
 188
 189 inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con.
 190
 191 (* UNEXPORTED
 192 End Field_axioms.
 193 *)
 194
 195 (* UNEXPORTED
 196 Section Field_basics.
 197 *)
 198
 199 (*#* ** Field basics
 200 %\begin{convention}% Let [F] be a field.
 201 %\end{convention}%
 202 *)
 203
 204 inline cic:/CoRN/algebra/CFields/F.var.
 205
 206 inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con.
 207
 208 inline cic:/CoRN/algebra/CFields/field_mult_inv.con.
 209
 210 (* UNEXPORTED
 211 Hint Resolve field_mult_inv: algebra.
 212 *)
 213
 214 inline cic:/CoRN/algebra/CFields/field_mult_inv_op.con.
 215
 216 (* UNEXPORTED
 217 End Field_basics.
 218 *)
 219
 220 (* UNEXPORTED
 221 Hint Resolve field_mult_inv field_mult_inv_op: algebra.
 222 *)
 223
 224 (* UNEXPORTED
 225 Section Field_multiplication.
 226 *)
 227
 228 (*#*
 229 ** Properties of multiplication
 230 %\begin{convention}% Let [F] be a field.
 231 %\end{convention}%
 232 *)
 233
 234 inline cic:/CoRN/algebra/CFields/F.var.
 235
 236 inline cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con.
 237
 238 inline cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con.
 239
 240 inline cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con.
 241
 242 inline cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con.
 243
 244 inline cic:/CoRN/algebra/CFields/mult_resp_neq.con.
 245
 246 inline cic:/CoRN/algebra/CFields/mult_eq_zero.con.
 247
 248 inline cic:/CoRN/algebra/CFields/mult_cancel_lft.con.
 249
 250 inline cic:/CoRN/algebra/CFields/mult_cancel_rht.con.
 251
 252 inline cic:/CoRN/algebra/CFields/square_eq_aux.con.
 253
 254 inline cic:/CoRN/algebra/CFields/square_eq_weak.con.
 255
 256 inline cic:/CoRN/algebra/CFields/cond_square_eq.con.
 257
 258 (* UNEXPORTED
 259 End Field_multiplication.
 260 *)
 261
 262 (* UNEXPORTED
 263 Section x_square.
 264 *)
 265
 266 inline cic:/CoRN/algebra/CFields/x_xminone.con.
 267
 268 inline cic:/CoRN/algebra/CFields/square_id.con.
 269
 270 (* UNEXPORTED
 271 End x_square.
 272 *)
 273
 274 (* UNEXPORTED
 275 Hint Resolve mult_resp_ap_zero: algebra.
 276 *)
 277
 278 (* UNEXPORTED
 279 Section Rcpcl_properties.
 280 *)
 281
 282 (*#*
 283 ** Properties of reciprocal
 284 %\begin{convention}% Let [F] be a field.
 285 %\end{convention}%
 286 *)
 287
 288 inline cic:/CoRN/algebra/CFields/F.var.
 289
 290 inline cic:/CoRN/algebra/CFields/inv_one.con.
 291
 292 inline cic:/CoRN/algebra/CFields/f_rcpcl_wd.con.
 293
 294 inline cic:/CoRN/algebra/CFields/f_rcpcl_mult.con.
 295
 296 inline cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con.
 297
 298 inline cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con.
 299
 300 (* UNEXPORTED
 301 End Rcpcl_properties.
 302 *)
 303
 304 (* UNEXPORTED
 305 Section MultipGroup.
 306 *)
 307
 308 (*#*
 309 ** The multiplicative group of nonzeros of a field.
 310 %\begin{convention}% Let [F] be a field
 311 %\end{convention}%
 312 *)
 313
 314 inline cic:/CoRN/algebra/CFields/F.var.
 315
 316 (*#*
 317 The multiplicative monoid of NonZeros.
 318 *)
 319
 320 inline cic:/CoRN/algebra/CFields/NonZeroMonoid.con.
 321
 322 inline cic:/CoRN/algebra/CFields/fmg_cs_inv.con.
 323
 324 inline cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con.
 325
 326 inline cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con.
 327
 328 (* UNEXPORTED
 329 End MultipGroup.
 330 *)
 331
 332 (* UNEXPORTED
 333 Section Div_properties.
 334 *)
 335
 336 (*#*
 337 ** Properties of division
 338 %\begin{convention}% Let [F] be a field.
 339 %\end{convention}%
 340
 341 %\begin{nameconvention}%
 342 In the names of lemmas, we denote [[/]] by [div], and
 343 [One[/]] by [recip].
 344 %\end{nameconvention}%
 345 *)
 346
 347 inline cic:/CoRN/algebra/CFields/F.var.
 348
 349 inline cic:/CoRN/algebra/CFields/div_prop.con.
 350
 351 inline cic:/CoRN/algebra/CFields/div_1.con.
 352
 353 inline cic:/CoRN/algebra/CFields/div_1'.con.
 354
 355 inline cic:/CoRN/algebra/CFields/div_1''.con.
 356
 357 (* UNEXPORTED
 358 Hint Resolve div_1: algebra.
 359 *)
 360
 361 inline cic:/CoRN/algebra/CFields/x_div_x.con.
 362
 363 (* UNEXPORTED
 364 Hint Resolve x_div_x: algebra.
 365 *)
 366
 367 inline cic:/CoRN/algebra/CFields/x_div_one.con.
 368
 369 (*#*
 370 The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$
 371 #x.(y/z) = (x.y)/z#.
 372 *)
 373
 374 inline cic:/CoRN/algebra/CFields/x_mult_y_div_z.con.
 375
 376 (* UNEXPORTED
 377 Hint Resolve x_mult_y_div_z: algebra.
 378 *)
 379
 380 inline cic:/CoRN/algebra/CFields/div_wd.con.
 381
 382 (* UNEXPORTED
 383 Hint Resolve div_wd: algebra_c.
 384 *)
 385
 386 (*#*
 387 The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$
 388 #[(x/y)/z = x/(y.z)]#
 389 *)
 390
 391 inline cic:/CoRN/algebra/CFields/div_div.con.
 392
 393 inline cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con.
 394
 395 inline cic:/CoRN/algebra/CFields/div_resp_ap_zero.con.
 396
 397 (*#*
 398 The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$
 399 #[x/(y/z) = (x.z)/y]#
 400 *)
 401
 402 inline cic:/CoRN/algebra/CFields/div_div2.con.
 403
 404 (*#*
 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)]#
 407 *)
 408
 409 inline cic:/CoRN/algebra/CFields/mult_of_divs.con.
 410
 411 inline cic:/CoRN/algebra/CFields/div_dist.con.
 412
 413 inline cic:/CoRN/algebra/CFields/div_dist'.con.
 414
 415 inline cic:/CoRN/algebra/CFields/div_semi_sym.con.
 416
 417 (* UNEXPORTED
 418 Hint Resolve div_semi_sym: algebra.
 419 *)
 420
 421 inline cic:/CoRN/algebra/CFields/eq_div.con.
 422
 423 inline cic:/CoRN/algebra/CFields/div_strext.con.
 424
 425 (* UNEXPORTED
 426 End Div_properties.
 427 *)
 428
 429 (* UNEXPORTED
 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
 432   div_prop: algebra.
 433 *)
 434
 435 (*#*
 436 ** Cancellation laws for apartness and multiplication
 437 %\begin{convention}% Let [F] be a field
 438 %\end{convention}%
 439 *)
 440
 441 (* UNEXPORTED
 442 Section Mult_Cancel_Ap_Zero.
 443 *)
 444
 445 inline cic:/CoRN/algebra/CFields/F.var.
 446
 447 inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con.
 448
 449 inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con.
 450
 451 inline cic:/CoRN/algebra/CFields/recip_ap_zero.con.
 452
 453 inline cic:/CoRN/algebra/CFields/recip_resp_ap.con.
 454
 455 (* UNEXPORTED
 456 End Mult_Cancel_Ap_Zero.
 457 *)
 458
 459 (* UNEXPORTED
 460 Section CField_Ops.
 461 *)
 462
 463 (*#*
 464 ** Functional Operations
 465
 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.
 470
 471 %\begin{convention}%
 472 Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively
 473 [P] and [Q].
 474 %\end{convention}%
 475 *)
 476
 477 inline cic:/CoRN/algebra/CFields/X.var.
 478
 479 inline cic:/CoRN/algebra/CFields/F.var.
 480
 481 inline cic:/CoRN/algebra/CFields/G.var.
 482
 483 (* begin hide *)
 484
 485 inline cic:/CoRN/algebra/CFields/P.con.
 486
 487 inline cic:/CoRN/algebra/CFields/Q.con.
 488
 489 (* end hide *)
 490
 491 (* UNEXPORTED
 492 Section Part_Function_Recip.
 493 *)
 494
 495 (*#*
 496 Some auxiliary notions are helpful in defining the domain.
 497 *)
 498
 499 inline cic:/CoRN/algebra/CFields/R.con.
 500
 501 inline cic:/CoRN/algebra/CFields/Ext2R.con.
 502
 503 inline cic:/CoRN/algebra/CFields/part_function_recip_strext.con.
 504
 505 inline cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con.
 506
 507 inline cic:/CoRN/algebra/CFields/Frecip.con.
 508
 509 (* UNEXPORTED
 510 End Part_Function_Recip.
 511 *)
 512
 513 (* UNEXPORTED
 514 Section Part_Function_Div.
 515 *)
 516
 517 (*#*
 518 For division things work out almost in the same way.
 519 *)
 520
 521 inline cic:/CoRN/algebra/CFields/R.con.
 522
 523 inline cic:/CoRN/algebra/CFields/Ext2R.con.
 524
 525 inline cic:/CoRN/algebra/CFields/part_function_div_strext.con.
 526
 527 inline cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con.
 528
 529 inline cic:/CoRN/algebra/CFields/Fdiv.con.
 530
 531 (* UNEXPORTED
 532 End Part_Function_Div.
 533 *)
 534
 535 (*#*
 536 %\begin{convention}% Let [R:X->CProp].
 537 %\end{convention}%
 538 *)
 539
 540 inline cic:/CoRN/algebra/CFields/R.var.
 541
 542 inline cic:/CoRN/algebra/CFields/included_FRecip.con.
 543
 544 inline cic:/CoRN/algebra/CFields/included_FRecip'.con.
 545
 546 inline cic:/CoRN/algebra/CFields/included_FDiv.con.
 547
 548 inline cic:/CoRN/algebra/CFields/included_FDiv'.con.
 549
 550 inline cic:/CoRN/algebra/CFields/included_FDiv''.con.
 551
 552 (* UNEXPORTED
 553 End CField_Ops.
 554 *)
 555
 556 (* UNEXPORTED
 557 Implicit Arguments Frecip [X].
 558 *)
 559
 560 (* UNEXPORTED
 561 Implicit Arguments Fdiv [X].
 562 *)
 563
 564 (* UNEXPORTED
 565 Hint Resolve included_FRecip included_FDiv : included.
 566 *)
 567
 568 (* UNEXPORTED
 569 Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included.
 570 *)
 571