helm/software/matita/contribs/procedural/CoRN/algebra/CRings.mma

   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 include "CoRN.ma".
  18
  19 (* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
  20
  21 (*#* printing [*] %\ensuremath\times% #&times;# *)
  22
  23 (*#* printing [^] %\ensuremath{\hat{\ }}% #^# *)
  24
  25 (*#* printing {*} %\ensuremath\times% #&times;# *)
  26
  27 (*#* printing {**} %\ensuremath\ast% #&lowast;# *)
  28
  29 (*#* printing {^} %\ensuremath{\hat{\ }}% #^# *)
  30
  31 (*#* printing One %\ensuremath{\mathbf1}% #1# *)
  32
  33 (*#* printing Two %\ensuremath{\mathbf2}% #2# *)
  34
  35 (*#* printing Three %\ensuremath{\mathbf3}% #3# *)
  36
  37 (*#* printing Four %\ensuremath{\mathbf4}% #4# *)
  38
  39 (*#* printing Six %\ensuremath{\mathbf6}% #6# *)
  40
  41 (*#* printing Eight %\ensuremath{\mathbf8}% #8# *)
  42
  43 (*#* printing Nine %\ensuremath{\mathbf9}% #9# *)
  44
  45 (*#* printing Twelve %\ensuremath{\mathbf{12}}% #12# *)
  46
  47 (*#* printing Sixteen %\ensuremath{\mathbf{16}}% #16# *)
  48
  49 (*#* printing Eighteen %\ensuremath{\mathbf{18}}% #18# *)
  50
  51 (*#* printing TwentyFour %\ensuremath{\mathbf{24}}% #24# *)
  52
  53 (*#* printing FortyEight %\ensuremath{\mathbf{48}}% #48# *)
  54
  55 include "algebra/CSums.ma".
  56
  57 (* UNEXPORTED
  58 Transparent sym_eq.
  59 *)
  60
  61 (* UNEXPORTED
  62 Transparent f_equal.
  63 *)
  64
  65 (* Begin_SpecReals *)
  66
  67 (* Constructive RINGS *)
  68
  69 (*#* * Rings
  70 We actually define commutative rings with identity.
  71 ** Definition of the notion of Ring
  72 *)
  73
  74 inline procedural "cic:/CoRN/algebra/CRings/distributive.con" as definition.
  75
  76 (* UNEXPORTED
  77 Implicit Arguments distributive [S].
  78 *)
  79
  80 inline procedural "cic:/CoRN/algebra/CRings/is_CRing.ind".
  81
  82 inline procedural "cic:/CoRN/algebra/CRings/CRing.ind".
  83
  84 (* COERCION
  85 cic:/matita/CoRN-Procedural/algebra/CRings/cr_crr.con
  86 *)
  87
  88 inline procedural "cic:/CoRN/algebra/CRings/cr_plus.con" as definition.
  89
  90 inline procedural "cic:/CoRN/algebra/CRings/cr_inv.con" as definition.
  91
  92 inline procedural "cic:/CoRN/algebra/CRings/cr_minus.con" as definition.
  93
  94 (* NOTATION
  95 Notation One := (cr_one _).
  96 *)
  97
  98 (* End_SpecReals *)
  99
 100 (* Begin_SpecReals *)
 101
 102 (*#*
 103 %\begin{nameconvention}%
 104 In the names of lemmas, we will denote [One] with [one],
 105 and [[*]] with [mult].
 106 %\end{nameconvention}%
 107 *)
 108
 109 (* UNEXPORTED
 110 Implicit Arguments cr_mult [c].
 111 *)
 112
 113 (* NOTATION
 114 Infix "[*]" := cr_mult (at level 40, left associativity).
 115 *)
 116
 117 (* UNEXPORTED
 118 Section CRing_axioms
 119 *)
 120
 121 (*#*
 122 ** Ring axioms
 123 %\begin{convention}% Let [R] be a ring.
 124 %\end{convention}%
 125 *)
 126
 127 (* UNEXPORTED
 128 cic:/CoRN/algebra/CRings/CRing_axioms/R.var
 129 *)
 130
 131 inline procedural "cic:/CoRN/algebra/CRings/CRing_is_CRing.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/algebra/CRings/mult_assoc.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/algebra/CRings/mult_commutes.con" as lemma.
 136
 137 inline procedural "cic:/CoRN/algebra/CRings/mult_mon.con" as lemma.
 138
 139 (* End_SpecReals *)
 140
 141 inline procedural "cic:/CoRN/algebra/CRings/dist.con" as lemma.
 142
 143 inline procedural "cic:/CoRN/algebra/CRings/ring_non_triv.con" as lemma.
 144
 145 inline procedural "cic:/CoRN/algebra/CRings/mult_wd.con" as lemma.
 146
 147 inline procedural "cic:/CoRN/algebra/CRings/mult_wdl.con" as lemma.
 148
 149 inline procedural "cic:/CoRN/algebra/CRings/mult_wdr.con" as lemma.
 150
 151 (* Begin_SpecReals *)
 152
 153 (* UNEXPORTED
 154 End CRing_axioms
 155 *)
 156
 157 (* UNEXPORTED
 158 Section Ring_constructions
 159 *)
 160
 161 (*#*
 162 ** Ring constructions
 163 %\begin{convention}%
 164 Let [R] be a ring.
 165 %\end{convention}%
 166 *)
 167
 168 (* UNEXPORTED
 169 cic:/CoRN/algebra/CRings/Ring_constructions/R.var
 170 *)
 171
 172 (*#*
 173 The multiplicative monoid of a ring is defined as follows.
 174 *)
 175
 176 inline procedural "cic:/CoRN/algebra/CRings/Build_multCMonoid.con" as definition.
 177
 178 (* UNEXPORTED
 179 End Ring_constructions
 180 *)
 181
 182 (* End_SpecReals *)
 183
 184 (* UNEXPORTED
 185 Section Ring_unfolded
 186 *)
 187
 188 (*#*
 189 ** Ring unfolded
 190 %\begin{convention}% Let [R] be a ring.
 191 %\end{convention}%
 192 *)
 193
 194 (* UNEXPORTED
 195 cic:/CoRN/algebra/CRings/Ring_unfolded/R.var
 196 *)
 197
 198 (* begin hide *)
 199
 200 inline procedural "cic:/CoRN/algebra/CRings/Ring_unfolded/mmR.con" "Ring_unfolded__" as definition.
 201
 202 (* end hide *)
 203
 204 inline procedural "cic:/CoRN/algebra/CRings/mult_assoc_unfolded.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/algebra/CRings/mult_commut_unfolded.con" as lemma.
 207
 208 (* UNEXPORTED
 209 Hint Resolve mult_commut_unfolded: algebra.
 210 *)
 211
 212 inline procedural "cic:/CoRN/algebra/CRings/mult_one.con" as lemma.
 213
 214 inline procedural "cic:/CoRN/algebra/CRings/one_mult.con" as lemma.
 215
 216 inline procedural "cic:/CoRN/algebra/CRings/ring_dist_unfolded.con" as lemma.
 217
 218 (* UNEXPORTED
 219 Hint Resolve ring_dist_unfolded: algebra.
 220 *)
 221
 222 inline procedural "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con" as lemma.
 223
 224 (* UNEXPORTED
 225 End Ring_unfolded
 226 *)
 227
 228 (* UNEXPORTED
 229 Hint Resolve mult_assoc_unfolded: algebra.
 230 *)
 231
 232 (* UNEXPORTED
 233 Hint Resolve ring_non_triv mult_one one_mult mult_commut_unfolded: algebra.
 234 *)
 235
 236 (* UNEXPORTED
 237 Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra.
 238 *)
 239
 240 (* UNEXPORTED
 241 Section Ring_basics
 242 *)
 243
 244 (*#*
 245 ** Ring basics
 246 %\begin{convention}% Let [R] be a ring.
 247 %\end{convention}%
 248 *)
 249
 250 (* UNEXPORTED
 251 cic:/CoRN/algebra/CRings/Ring_basics/R.var
 252 *)
 253
 254 inline procedural "cic:/CoRN/algebra/CRings/one_ap_zero.con" as lemma.
 255
 256 inline procedural "cic:/CoRN/algebra/CRings/is_zero_rht.con" as definition.
 257
 258 inline procedural "cic:/CoRN/algebra/CRings/is_zero_lft.con" as definition.
 259
 260 (* UNEXPORTED
 261 Implicit Arguments is_zero_rht [S].
 262 *)
 263
 264 (* UNEXPORTED
 265 Implicit Arguments is_zero_lft [S].
 266 *)
 267
 268 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_zero.con" as lemma.
 269
 270 (* UNEXPORTED
 271 Hint Resolve cring_mult_zero: algebra.
 272 *)
 273
 274 inline procedural "cic:/CoRN/algebra/CRings/x_mult_zero.con" as lemma.
 275
 276 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_zero_op.con" as lemma.
 277
 278 (* UNEXPORTED
 279 Hint Resolve cring_mult_zero_op: algebra.
 280 *)
 281
 282 inline procedural "cic:/CoRN/algebra/CRings/cring_inv_mult_lft.con" as lemma.
 283
 284 (* UNEXPORTED
 285 Hint Resolve cring_inv_mult_lft: algebra.
 286 *)
 287
 288 inline procedural "cic:/CoRN/algebra/CRings/cring_inv_mult_rht.con" as lemma.
 289
 290 (* UNEXPORTED
 291 Hint Resolve cring_inv_mult_rht: algebra.
 292 *)
 293
 294 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_ap_zero.con" as lemma.
 295
 296 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_ap_zero_op.con" as lemma.
 297
 298 inline procedural "cic:/CoRN/algebra/CRings/inv_mult_invol.con" as lemma.
 299
 300 inline procedural "cic:/CoRN/algebra/CRings/ring_dist_minus.con" as lemma.
 301
 302 (* UNEXPORTED
 303 Hint Resolve ring_dist_minus: algebra.
 304 *)
 305
 306 inline procedural "cic:/CoRN/algebra/CRings/ring_distl_minus.con" as lemma.
 307
 308 (* UNEXPORTED
 309 Hint Resolve ring_distl_minus: algebra.
 310 *)
 311
 312 (* UNEXPORTED
 313 End Ring_basics
 314 *)
 315
 316 (* UNEXPORTED
 317 Hint Resolve cring_mult_zero cring_mult_zero_op: algebra.
 318 *)
 319
 320 (* UNEXPORTED
 321 Hint Resolve inv_mult_invol: algebra.
 322 *)
 323
 324 (* UNEXPORTED
 325 Hint Resolve cring_inv_mult_lft cring_inv_mult_rht: algebra.
 326 *)
 327
 328 (* UNEXPORTED
 329 Hint Resolve ring_dist_minus: algebra.
 330 *)
 331
 332 (* UNEXPORTED
 333 Hint Resolve ring_distl_minus: algebra.
 334 *)
 335
 336 (* Begin_SpecReals *)
 337
 338 (*#*
 339 ** Ring Definitions
 340 Some auxiliary functions and operations over a ring;
 341 especially geared towards CReals.
 342 *)
 343
 344 (* UNEXPORTED
 345 Section exponentiation
 346 *)
 347
 348 (*#*
 349 *** Exponentiation
 350 %\begin{convention}%
 351 Let [R] be a ring.
 352 %\end{convention}%
 353 *)
 354
 355 (* UNEXPORTED
 356 cic:/CoRN/algebra/CRings/exponentiation/R.var
 357 *)
 358
 359 (* End_SpecReals *)
 360
 361 inline procedural "cic:/CoRN/algebra/CRings/nexp.con" as definition.
 362
 363 inline procedural "cic:/CoRN/algebra/CRings/nexp_well_def.con" as lemma.
 364
 365 inline procedural "cic:/CoRN/algebra/CRings/nexp_strong_ext.con" as lemma.
 366
 367 inline procedural "cic:/CoRN/algebra/CRings/nexp_op.con" as definition.
 368
 369 (* Begin_SpecReals *)
 370
 371 (* UNEXPORTED
 372 End exponentiation
 373 *)
 374
 375 (* End_SpecReals *)
 376
 377 (* NOTATION
 378 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
 379 *)
 380
 381 (* UNEXPORTED
 382 Implicit Arguments nexp_op [R].
 383 *)
 384
 385 (* Begin_SpecReals *)
 386
 387 (* UNEXPORTED
 388 Section nat_injection
 389 *)
 390
 391 (*#*
 392 *** The injection of natural numbers into a ring
 393 %\begin{convention}% Let [R] be a ring.
 394 %\end{convention}%
 395 *)
 396
 397 (* UNEXPORTED
 398 cic:/CoRN/algebra/CRings/nat_injection/R.var
 399 *)
 400
 401 (*#*
 402 The injection of Coq natural numbers into a ring is called [nring].
 403 Note that this need not really be an injection; when it is, the ring is said
 404 to have characteristic [0].
 405 *)
 406
 407 inline procedural "cic:/CoRN/algebra/CRings/nring.con" as definition.
 408
 409 inline procedural "cic:/CoRN/algebra/CRings/Char0.con" as definition.
 410
 411 (* End_SpecReals *)
 412
 413 inline procedural "cic:/CoRN/algebra/CRings/nring_comm_plus.con" as lemma.
 414
 415 inline procedural "cic:/CoRN/algebra/CRings/nring_comm_mult.con" as lemma.
 416
 417 (* Begin_SpecReals *)
 418
 419 (* UNEXPORTED
 420 End nat_injection
 421 *)
 422
 423 (* End_SpecReals *)
 424
 425 (* UNEXPORTED
 426 Hint Resolve nring_comm_plus nring_comm_mult: algebra.
 427 *)
 428
 429 (* Begin_SpecReals *)
 430
 431 (* UNEXPORTED
 432 Implicit Arguments nring [R].
 433 *)
 434
 435 (* End_SpecReals *)
 436
 437 (* NOTATION
 438 Notation Two := (nring 2).
 439 *)
 440
 441 (* NOTATION
 442 Notation Three := (nring 3).
 443 *)
 444
 445 (* NOTATION
 446 Notation Four := (nring 4).
 447 *)
 448
 449 (* NOTATION
 450 Notation Six := (nring 6).
 451 *)
 452
 453 (* NOTATION
 454 Notation Eight := (nring 8).
 455 *)
 456
 457 (* NOTATION
 458 Notation Twelve := (nring 12).
 459 *)
 460
 461 (* NOTATION
 462 Notation Sixteen := (nring 16).
 463 *)
 464
 465 (* NOTATION
 466 Notation Nine := (nring 9).
 467 *)
 468
 469 (* NOTATION
 470 Notation Eighteen := (nring 18).
 471 *)
 472
 473 (* NOTATION
 474 Notation TwentyFour := (nring 24).
 475 *)
 476
 477 (* NOTATION
 478 Notation FortyEight := (nring 48).
 479 *)
 480
 481 inline procedural "cic:/CoRN/algebra/CRings/one_plus_one.con" as lemma.
 482
 483 inline procedural "cic:/CoRN/algebra/CRings/x_plus_x.con" as lemma.
 484
 485 (* UNEXPORTED
 486 Hint Resolve one_plus_one x_plus_x: algebra.
 487 *)
 488
 489 (*#*
 490 In a ring of characteristic zero, [nring] is really an injection.
 491 *)
 492
 493 inline procedural "cic:/CoRN/algebra/CRings/nring_different.con" as lemma.
 494
 495 (* UNEXPORTED
 496 Section int_injection
 497 *)
 498
 499 (*#*
 500 *** The injection of integers into a ring
 501 %\begin{convention}%
 502 Let [R] be a ring.
 503 %\end{convention}%
 504 *)
 505
 506 (* UNEXPORTED
 507 cic:/CoRN/algebra/CRings/int_injection/R.var
 508 *)
 509
 510 (*#*
 511 The injection of Coq integers into a ring is called [zring]. Again,
 512 this need not really be an injection.
 513
 514 The first definition is now obsolete, having been replaced by a more efficient
 515 one. It is kept to avoid having to redo all the proofs.
 516 *)
 517
 518 inline procedural "cic:/CoRN/algebra/CRings/zring_old.con" as definition.
 519
 520 inline procedural "cic:/CoRN/algebra/CRings/zring_old_zero.con" as lemma.
 521
 522 (* UNEXPORTED
 523 Hint Resolve zring_old_zero: algebra.
 524 *)
 525
 526 inline procedural "cic:/CoRN/algebra/CRings/zring_old_diff.con" as lemma.
 527
 528 (* UNEXPORTED
 529 Hint Resolve zring_old_diff.
 530 *)
 531
 532 inline procedural "cic:/CoRN/algebra/CRings/zring_old_plus_nat.con" as lemma.
 533
 534 (* UNEXPORTED
 535 Hint Resolve zring_old_plus_nat: algebra.
 536 *)
 537
 538 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv_nat.con" as lemma.
 539
 540 (* UNEXPORTED
 541 Hint Resolve zring_old_inv_nat: algebra.
 542 *)
 543
 544 (* UNEXPORTED
 545 Hint Resolve zring_old_diff: algebra.
 546 *)
 547
 548 inline procedural "cic:/CoRN/algebra/CRings/zring_old_plus.con" as lemma.
 549
 550 (* UNEXPORTED
 551 Hint Resolve zring_old_plus: algebra.
 552 *)
 553
 554 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv.con" as lemma.
 555
 556 (* UNEXPORTED
 557 Hint Resolve zring_old_inv: algebra.
 558 *)
 559
 560 inline procedural "cic:/CoRN/algebra/CRings/zring_old_minus.con" as lemma.
 561
 562 (* UNEXPORTED
 563 Hint Resolve zring_old_minus: algebra.
 564 *)
 565
 566 inline procedural "cic:/CoRN/algebra/CRings/zring_old_mult.con" as lemma.
 567
 568 (* UNEXPORTED
 569 Hint Resolve zring_old_mult: algebra.
 570 *)
 571
 572 inline procedural "cic:/CoRN/algebra/CRings/zring_old_one.con" as lemma.
 573
 574 (* UNEXPORTED
 575 Hint Resolve zring_old_one: algebra.
 576 *)
 577
 578 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv_one.con" as lemma.
 579
 580 (*#************** new def of zring. ***********************)
 581
 582 (*#* The [zring] function can be defined directly.  This is done here.
 583 *)
 584
 585 inline procedural "cic:/CoRN/algebra/CRings/pring_aux.con" as definition.
 586
 587 inline procedural "cic:/CoRN/algebra/CRings/pring.con" as definition.
 588
 589 inline procedural "cic:/CoRN/algebra/CRings/zring.con" as definition.
 590
 591 inline procedural "cic:/CoRN/algebra/CRings/pring_aux_lemma.con" as lemma.
 592
 593 inline procedural "cic:/CoRN/algebra/CRings/double_nring.con" as lemma.
 594
 595 (* UNEXPORTED
 596 Hint Resolve pring_aux_lemma double_nring: algebra.
 597 *)
 598
 599 inline procedural "cic:/CoRN/algebra/CRings/pring_aux_nring.con" as lemma.
 600
 601 (* UNEXPORTED
 602 Hint Resolve pring_aux_nring: algebra.
 603 *)
 604
 605 inline procedural "cic:/CoRN/algebra/CRings/pring_convert.con" as lemma.
 606
 607 (* UNEXPORTED
 608 Hint Resolve pring_convert: algebra.
 609 *)
 610
 611 inline procedural "cic:/CoRN/algebra/CRings/zring_zring_old.con" as lemma.
 612
 613 (* UNEXPORTED
 614 Hint Resolve zring_zring_old: algebra.
 615 *)
 616
 617 inline procedural "cic:/CoRN/algebra/CRings/zring_zero.con" as lemma.
 618
 619 inline procedural "cic:/CoRN/algebra/CRings/zring_diff.con" as lemma.
 620
 621 inline procedural "cic:/CoRN/algebra/CRings/zring_plus_nat.con" as lemma.
 622
 623 inline procedural "cic:/CoRN/algebra/CRings/zring_inv_nat.con" as lemma.
 624
 625 inline procedural "cic:/CoRN/algebra/CRings/zring_plus.con" as lemma.
 626
 627 inline procedural "cic:/CoRN/algebra/CRings/zring_inv.con" as lemma.
 628
 629 inline procedural "cic:/CoRN/algebra/CRings/zring_minus.con" as lemma.
 630
 631 inline procedural "cic:/CoRN/algebra/CRings/zring_mult.con" as lemma.
 632
 633 inline procedural "cic:/CoRN/algebra/CRings/zring_one.con" as lemma.
 634
 635 inline procedural "cic:/CoRN/algebra/CRings/zring_inv_one.con" as lemma.
 636
 637 (* UNEXPORTED
 638 End int_injection
 639 *)
 640
 641 (* UNEXPORTED
 642 Implicit Arguments zring [R].
 643 *)
 644
 645 (* UNEXPORTED
 646 Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat
 647   zring_plus zring_inv zring_minus zring_mult zring_one zring_inv_one:
 648   algebra.
 649 *)
 650
 651 (* UNEXPORTED
 652 Section Ring_sums
 653 *)
 654
 655 (*#*
 656 ** Ring sums
 657 %\begin{convention}% Let [R] be a ring.
 658 %\end{convention}%
 659 *)
 660
 661 (* UNEXPORTED
 662 cic:/CoRN/algebra/CRings/Ring_sums/R.var
 663 *)
 664
 665 (*#*
 666 *** Infinite Ring sums
 667 *)
 668
 669 (* UNEXPORTED
 670 Section infinite_ring_sums
 671 *)
 672
 673 inline procedural "cic:/CoRN/algebra/CRings/Sum_upto.con" as definition.
 674
 675 inline procedural "cic:/CoRN/algebra/CRings/sum_upto_O.con" as lemma.
 676
 677 inline procedural "cic:/CoRN/algebra/CRings/Sum_from_upto.con" as definition.
 678
 679 (*#*
 680 Here's an alternative def of [Sum_from_upto], with a lemma that
 681 it's equivalent to the original.
 682 *)
 683
 684 inline procedural "cic:/CoRN/algebra/CRings/seq_from.con" as definition.
 685
 686 inline procedural "cic:/CoRN/algebra/CRings/Sum_from_upto_alt.con" as definition.
 687
 688 (* UNEXPORTED
 689 End infinite_ring_sums
 690 *)
 691
 692 (* UNEXPORTED
 693 Section ring_sums_over_lists
 694 *)
 695
 696 (*#* *** Ring Sums over Lists
 697 *)
 698
 699 inline procedural "cic:/CoRN/algebra/CRings/RList_Mem.con" as definition.
 700
 701 inline procedural "cic:/CoRN/algebra/CRings/List_Sum_upto.con" as definition.
 702
 703 inline procedural "cic:/CoRN/algebra/CRings/list_sum_upto_O.con" as lemma.
 704
 705 inline procedural "cic:/CoRN/algebra/CRings/List_Sum_from_upto.con" as definition.
 706
 707 (* UNEXPORTED
 708 End ring_sums_over_lists
 709 *)
 710
 711 (* UNEXPORTED
 712 End Ring_sums
 713 *)
 714
 715 (*#*
 716 ** Distribution properties
 717 %\begin{convention}%
 718 Let [R] be a ring.
 719 %\end{convention}%
 720 *)
 721
 722 (* UNEXPORTED
 723 Section Dist_properties
 724 *)
 725
 726 (* UNEXPORTED
 727 cic:/CoRN/algebra/CRings/Dist_properties/R.var
 728 *)
 729
 730 inline procedural "cic:/CoRN/algebra/CRings/dist_1b.con" as lemma.
 731
 732 (* UNEXPORTED
 733 Hint Resolve dist_1b: algebra.
 734 *)
 735
 736 inline procedural "cic:/CoRN/algebra/CRings/dist_2a.con" as lemma.
 737
 738 (* UNEXPORTED
 739 Hint Resolve dist_2a: algebra.
 740 *)
 741
 742 inline procedural "cic:/CoRN/algebra/CRings/dist_2b.con" as lemma.
 743
 744 (* UNEXPORTED
 745 Hint Resolve dist_2b: algebra.
 746 *)
 747
 748 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum0_lft.con" as lemma.
 749
 750 (* UNEXPORTED
 751 Hint Resolve mult_distr_sum0_lft.
 752 *)
 753
 754 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum_lft.con" as lemma.
 755
 756 (* UNEXPORTED
 757 Hint Resolve mult_distr_sum_lft: algebra.
 758 *)
 759
 760 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum_rht.con" as lemma.
 761
 762 inline procedural "cic:/CoRN/algebra/CRings/sumx_const.con" as lemma.
 763
 764 (* UNEXPORTED
 765 End Dist_properties
 766 *)
 767
 768 (* UNEXPORTED
 769 Hint Resolve dist_1b dist_2a dist_2b mult_distr_sum_lft mult_distr_sum_rht
 770   sumx_const: algebra.
 771 *)
 772
 773 (*#*
 774 ** Properties of exponentiation (with the exponent in [nat])
 775 %\begin{convention}%
 776 Let [R] be a ring.
 777 %\end{convention}%
 778 *)
 779
 780 (* UNEXPORTED
 781 Section NExp_properties
 782 *)
 783
 784 (* UNEXPORTED
 785 cic:/CoRN/algebra/CRings/NExp_properties/R.var
 786 *)
 787
 788 inline procedural "cic:/CoRN/algebra/CRings/nexp_wd.con" as lemma.
 789
 790 inline procedural "cic:/CoRN/algebra/CRings/nexp_strext.con" as lemma.
 791
 792 inline procedural "cic:/CoRN/algebra/CRings/nexp_Sn.con" as lemma.
 793
 794 (* UNEXPORTED
 795 Hint Resolve nexp_wd nexp_Sn: algebra.
 796 *)
 797
 798 inline procedural "cic:/CoRN/algebra/CRings/nexp_plus.con" as lemma.
 799
 800 (* UNEXPORTED
 801 Hint Resolve nexp_plus: algebra.
 802 *)
 803
 804 inline procedural "cic:/CoRN/algebra/CRings/one_nexp.con" as lemma.
 805
 806 (* UNEXPORTED
 807 Hint Resolve one_nexp: algebra.
 808 *)
 809
 810 inline procedural "cic:/CoRN/algebra/CRings/mult_nexp.con" as lemma.
 811
 812 (* UNEXPORTED
 813 Hint Resolve mult_nexp: algebra.
 814 *)
 815
 816 inline procedural "cic:/CoRN/algebra/CRings/nexp_mult.con" as lemma.
 817
 818 (* UNEXPORTED
 819 Hint Resolve nexp_mult: algebra.
 820 *)
 821
 822 inline procedural "cic:/CoRN/algebra/CRings/zero_nexp.con" as lemma.
 823
 824 (* UNEXPORTED
 825 Hint Resolve zero_nexp: algebra.
 826 *)
 827
 828 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_even.con" as lemma.
 829
 830 (* UNEXPORTED
 831 Hint Resolve inv_nexp_even: algebra.
 832 *)
 833
 834 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_two.con" as lemma.
 835
 836 (* UNEXPORTED
 837 Hint Resolve inv_nexp_two: algebra.
 838 *)
 839
 840 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_odd.con" as lemma.
 841
 842 (* UNEXPORTED
 843 Hint Resolve inv_nexp_odd: algebra.
 844 *)
 845
 846 inline procedural "cic:/CoRN/algebra/CRings/nexp_one.con" as lemma.
 847
 848 (* UNEXPORTED
 849 Hint Resolve nexp_one: algebra.
 850 *)
 851
 852 inline procedural "cic:/CoRN/algebra/CRings/nexp_two.con" as lemma.
 853
 854 (* UNEXPORTED
 855 Hint Resolve nexp_two: algebra.
 856 *)
 857
 858 inline procedural "cic:/CoRN/algebra/CRings/inv_one_even_nexp.con" as lemma.
 859
 860 (* UNEXPORTED
 861 Hint Resolve inv_one_even_nexp: algebra.
 862 *)
 863
 864 inline procedural "cic:/CoRN/algebra/CRings/inv_one_odd_nexp.con" as lemma.
 865
 866 (* UNEXPORTED
 867 Hint Resolve inv_one_odd_nexp: algebra.
 868 *)
 869
 870 inline procedural "cic:/CoRN/algebra/CRings/square_plus.con" as lemma.
 871
 872 inline procedural "cic:/CoRN/algebra/CRings/square_minus.con" as lemma.
 873
 874 inline procedural "cic:/CoRN/algebra/CRings/nexp_funny.con" as lemma.
 875
 876 (* UNEXPORTED
 877 Hint Resolve nexp_funny: algebra.
 878 *)
 879
 880 inline procedural "cic:/CoRN/algebra/CRings/nexp_funny'.con" as lemma.
 881
 882 (* UNEXPORTED
 883 Hint Resolve nexp_funny': algebra.
 884 *)
 885
 886 (* UNEXPORTED
 887 End NExp_properties
 888 *)
 889
 890 (* UNEXPORTED
 891 Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp
 892   inv_nexp_even inv_nexp_two inv_nexp_odd nexp_one nexp_two nexp_funny
 893   inv_one_even_nexp inv_one_odd_nexp nexp_funny' one_nexp square_plus
 894   square_minus: algebra.
 895 *)
 896
 897 (* UNEXPORTED
 898 Section CRing_Ops
 899 *)
 900
 901 (*#*
 902 ** Functional Operations
 903
 904 Now for partial functions.
 905
 906 %\begin{convention}%
 907 Let [R] be a ring and let [F,G:(PartFunct R)] with predicates
 908 respectively [P] and [Q].
 909 %\end{convention}%
 910 *)
 911
 912 (* UNEXPORTED
 913 cic:/CoRN/algebra/CRings/CRing_Ops/R.var
 914 *)
 915
 916 (* UNEXPORTED
 917 cic:/CoRN/algebra/CRings/CRing_Ops/F.var
 918 *)
 919
 920 (* UNEXPORTED
 921 cic:/CoRN/algebra/CRings/CRing_Ops/G.var
 922 *)
 923
 924 (* begin hide *)
 925
 926 inline procedural "cic:/CoRN/algebra/CRings/CRing_Ops/P.con" "CRing_Ops__" as definition.
 927
 928 inline procedural "cic:/CoRN/algebra/CRings/CRing_Ops/Q.con" "CRing_Ops__" as definition.
 929
 930 (* end hide *)
 931
 932 (* UNEXPORTED
 933 Section Part_Function_Mult
 934 *)
 935
 936 inline procedural "cic:/CoRN/algebra/CRings/part_function_mult_strext.con" as lemma.
 937
 938 inline procedural "cic:/CoRN/algebra/CRings/Fmult.con" as definition.
 939
 940 (* UNEXPORTED
 941 End Part_Function_Mult
 942 *)
 943
 944 (* UNEXPORTED
 945 Section Part_Function_Nth_Power
 946 *)
 947
 948 (* UNEXPORTED
 949 cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var
 950 *)
 951
 952 inline procedural "cic:/CoRN/algebra/CRings/part_function_nth_strext.con" as lemma.
 953
 954 inline procedural "cic:/CoRN/algebra/CRings/Fnth.con" as definition.
 955
 956 (* UNEXPORTED
 957 End Part_Function_Nth_Power
 958 *)
 959
 960 (*#*
 961 %\begin{convention}% Let [R':R->CProp].
 962 %\end{convention}%
 963 *)
 964
 965 (* UNEXPORTED
 966 cic:/CoRN/algebra/CRings/CRing_Ops/R'.var
 967 *)
 968
 969 inline procedural "cic:/CoRN/algebra/CRings/included_FMult.con" as lemma.
 970
 971 inline procedural "cic:/CoRN/algebra/CRings/included_FMult'.con" as lemma.
 972
 973 inline procedural "cic:/CoRN/algebra/CRings/included_FMult''.con" as lemma.
 974
 975 (* UNEXPORTED
 976 cic:/CoRN/algebra/CRings/CRing_Ops/n.var
 977 *)
 978
 979 inline procedural "cic:/CoRN/algebra/CRings/included_FNth.con" as lemma.
 980
 981 inline procedural "cic:/CoRN/algebra/CRings/included_FNth'.con" as lemma.
 982
 983 (* UNEXPORTED
 984 End CRing_Ops
 985 *)
 986
 987 inline procedural "cic:/CoRN/algebra/CRings/Fscalmult.con" as definition.
 988
 989 (* UNEXPORTED
 990 Implicit Arguments Fmult [R].
 991 *)
 992
 993 (* NOTATION
 994 Infix "{*}" := Fmult (at level 40, left associativity).
 995 *)
 996
 997 (* UNEXPORTED
 998 Implicit Arguments Fscalmult [R].
 999 *)
1000
1001 (* NOTATION
1002 Infix "{**}" := Fscalmult (at level 40, left associativity).
1003 *)
1004
1005 (* UNEXPORTED
1006 Implicit Arguments Fnth [R].
1007 *)
1008
1009 (* NOTATION
1010 Infix "{^}" := Fnth (at level 30, right associativity).
1011 *)
1012
1013 (* UNEXPORTED
1014 Section ScalarMultiplication
1015 *)
1016
1017 (* UNEXPORTED
1018 cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var
1019 *)
1020
1021 (* UNEXPORTED
1022 cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var
1023 *)
1024
1025 (* begin hide *)
1026
1027 inline procedural "cic:/CoRN/algebra/CRings/ScalarMultiplication/P.con" "ScalarMultiplication__" as definition.
1028
1029 (* end hide *)
1030
1031 (* UNEXPORTED
1032 cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var
1033 *)
1034
1035 inline procedural "cic:/CoRN/algebra/CRings/included_FScalMult.con" as lemma.
1036
1037 inline procedural "cic:/CoRN/algebra/CRings/included_FScalMult'.con" as lemma.
1038
1039 (* UNEXPORTED
1040 End ScalarMultiplication
1041 *)
1042
1043 (* UNEXPORTED
1044 Hint Resolve included_FMult included_FScalMult included_FNth : included.
1045 *)
1046
1047 (* UNEXPORTED
1048 Hint Immediate included_FMult' included_FMult'' included_FScalMult'
1049     included_FNth' : included.
1050 *)
1051