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