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