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