helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.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/complex/NRootCC".
  18
  19 (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
  20
  21 (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *)
  22
  23 (*#* printing sqrt_I %\ensuremath{\sqrt{\imath}}% *)
  24
  25 (*#* printing nroot_I %\ensuremath{\sqrt[n]{\imath}}% *)
  26
  27 (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
  28
  29 (* INCLUDE
  30 CComplex
  31 *)
  32
  33 (* INCLUDE
  34 Wf_nat
  35 *)
  36
  37 (* INCLUDE
  38 ArithRing
  39 *)
  40
  41 (*#* * Roots of Complex Numbers
  42
  43 Properties of non-zero complex numbers
  44 *)
  45
  46 (* UNEXPORTED
  47 Section CC_ap_zero.
  48 *)
  49
  50 inline cic:/CoRN/complex/NRootCC/cc_ap_zero.con.
  51
  52 inline cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con.
  53
  54 (* UNEXPORTED
  55 End CC_ap_zero.
  56 *)
  57
  58 (*#* Weird lemma. *)
  59
  60 (* UNEXPORTED
  61 Section Imag_to_Real.
  62 *)
  63
  64 inline cic:/CoRN/complex/NRootCC/imag_to_real.con.
  65
  66 (* UNEXPORTED
  67 End Imag_to_Real.
  68 *)
  69
  70 (*#* ** Roots of the imaginary unit *)
  71
  72 (* UNEXPORTED
  73 Section NRootI.
  74 *)
  75
  76 inline cic:/CoRN/complex/NRootCC/sqrt_Half.con.
  77
  78 inline cic:/CoRN/complex/NRootCC/sqrt_I.con.
  79
  80 inline cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con.
  81
  82 inline cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con.
  83
  84 inline cic:/CoRN/complex/NRootCC/nroot_I.con.
  85
  86 inline cic:/CoRN/complex/NRootCC/nroot_I_nexp.con.
  87
  88 (* UNEXPORTED
  89 Hint Resolve nroot_I_nexp: algebra.
  90 *)
  91
  92 inline cic:/CoRN/complex/NRootCC/nroot_minus_I.con.
  93
  94 inline cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con.
  95
  96 (* UNEXPORTED
  97 End NRootI.
  98 *)
  99
 100 (*#* ** Roots of complex numbers *)
 101
 102 (* UNEXPORTED
 103 Section NRootCC_1.
 104 *)
 105
 106 (*#* We define the nth root of a complex number with a non zero imaginary part.
 107 *)
 108
 109 (* UNEXPORTED
 110 Section NRootCC_1_ap_real.
 111 *)
 112
 113 (*#*
 114 %\begin{convention}% Let [a,b : IR] and [b_ : (b [#] Zero)].
 115 Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
 116 [a' := sqrt a'2], [b'2 := (c[-]a) [*]Half] and [b' := sqrt b'2].
 117 %\end{convention}%
 118 *)
 119
 120 inline cic:/CoRN/complex/NRootCC/a.var.
 121
 122 inline cic:/CoRN/complex/NRootCC/b.var.
 123
 124 inline cic:/CoRN/complex/NRootCC/b_.var.
 125
 126 (* begin hide *)
 127
 128 inline cic:/CoRN/complex/NRootCC/c2.con.
 129
 130 (* end hide *)
 131
 132 inline cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con.
 133
 134 (* begin hide *)
 135
 136 inline cic:/CoRN/complex/NRootCC/c.con.
 137
 138 inline cic:/CoRN/complex/NRootCC/a'2.con.
 139
 140 (* end hide *)
 141
 142 inline cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con.
 143
 144 (* begin hide *)
 145
 146 inline cic:/CoRN/complex/NRootCC/a'.con.
 147
 148 inline cic:/CoRN/complex/NRootCC/b'2.con.
 149
 150 (* end hide *)
 151
 152 inline cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con.
 153
 154 (* begin hide *)
 155
 156 inline cic:/CoRN/complex/NRootCC/b'.con.
 157
 158 (* end hide *)
 159
 160 inline cic:/CoRN/complex/NRootCC/nrCC1_a3.con.
 161
 162 inline cic:/CoRN/complex/NRootCC/nrCC1_a4.con.
 163
 164 (* UNEXPORTED
 165 Hint Resolve nrCC1_a4: algebra.
 166 *)
 167
 168 inline cic:/CoRN/complex/NRootCC/nrCC1_a5.con.
 169
 170 inline cic:/CoRN/complex/NRootCC/nrCC1_a6.con.
 171
 172 inline cic:/CoRN/complex/NRootCC/nrCC1_a6'.con.
 173
 174 (* UNEXPORTED
 175 Hint Resolve nrCC1_a5: algebra.
 176 *)
 177
 178 inline cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con.
 179
 180 inline cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con.
 181
 182 (* UNEXPORTED
 183 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
 184 *)
 185
 186 inline cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con.
 187
 188 inline cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con.
 189
 190 inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con.
 191
 192 (* UNEXPORTED
 193 End NRootCC_1_ap_real.
 194 *)
 195
 196 (*#* We now define the nth root of a complex number with a non zero real part.
 197 *)
 198
 199 (* UNEXPORTED
 200 Section NRootCC_1_ap_imag.
 201 *)
 202
 203 (*#*
 204 %\begin{convention}% Let [a,b : IR] and [a_ : (a [#] Zero)] and define
 205 [c' := (a[+I*]b) [*][--]II := a'[+I*]b'].
 206 %\end{convention}%
 207 *)
 208
 209 inline cic:/CoRN/complex/NRootCC/a.var.
 210
 211 inline cic:/CoRN/complex/NRootCC/b.var.
 212
 213 inline cic:/CoRN/complex/NRootCC/a_.var.
 214
 215 (* begin hide *)
 216
 217 inline cic:/CoRN/complex/NRootCC/c'.con.
 218
 219 inline cic:/CoRN/complex/NRootCC/a'.con.
 220
 221 inline cic:/CoRN/complex/NRootCC/b'.con.
 222
 223 (* end hide *)
 224
 225 (* UNEXPORTED
 226 Hint Resolve sqrt_I_nexp: algebra.
 227 *)
 228
 229 inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con.
 230
 231 (* UNEXPORTED
 232 End NRootCC_1_ap_imag.
 233 *)
 234
 235 (*#* We now define the roots of arbitrary non zero complex numbers. *)
 236
 237 inline cic:/CoRN/complex/NRootCC/nrootCC_1.con.
 238
 239 (* UNEXPORTED
 240 End NRootCC_1.
 241 *)
 242
 243 (* UNEXPORTED
 244 Section NRootCC_2.
 245 *)
 246
 247 (*#*
 248 %\begin{convention}% Let [n : nat] and [c,z : CC] and [c_:(c [#] Zero)].
 249 %\end{convention}%
 250 *)
 251
 252 inline cic:/CoRN/complex/NRootCC/n.var.
 253
 254 inline cic:/CoRN/complex/NRootCC/c.var.
 255
 256 inline cic:/CoRN/complex/NRootCC/z.var.
 257
 258 inline cic:/CoRN/complex/NRootCC/c_.var.
 259
 260 inline cic:/CoRN/complex/NRootCC/nrootCC_2'.con.
 261
 262 inline cic:/CoRN/complex/NRootCC/nrootCC_2.con.
 263
 264 (* UNEXPORTED
 265 End NRootCC_2.
 266 *)
 267
 268 (* UNEXPORTED
 269 Section NRootCC_3.
 270 *)
 271
 272 inline cic:/CoRN/complex/NRootCC/Im_poly.con.
 273
 274 inline cic:/CoRN/complex/NRootCC/nrCC3_a1.con.
 275
 276 inline cic:/CoRN/complex/NRootCC/nrCC3_a2.con.
 277
 278 (*#*
 279 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
 280 %\end{convention}%
 281 *)
 282
 283 inline cic:/CoRN/complex/NRootCC/a.var.
 284
 285 inline cic:/CoRN/complex/NRootCC/b.var.
 286
 287 inline cic:/CoRN/complex/NRootCC/b_.var.
 288
 289 inline cic:/CoRN/complex/NRootCC/n.var.
 290
 291 inline cic:/CoRN/complex/NRootCC/nrCC3_poly''.con.
 292
 293 inline cic:/CoRN/complex/NRootCC/nrCC3_a3.con.
 294
 295 inline cic:/CoRN/complex/NRootCC/nrCC3_a4.con.
 296
 297 inline cic:/CoRN/complex/NRootCC/nrCC3_a5.con.
 298
 299 inline cic:/CoRN/complex/NRootCC/nrCC3_a6.con.
 300
 301 inline cic:/CoRN/complex/NRootCC/nrCC3_poly'.con.
 302
 303 (* UNEXPORTED
 304 Hint Resolve nrCC3_a3: algebra.
 305 *)
 306
 307 inline cic:/CoRN/complex/NRootCC/nrCC3_a7.con.
 308
 309 inline cic:/CoRN/complex/NRootCC/nrCC3_a8.con.
 310
 311 (* UNEXPORTED
 312 Hint Resolve nth_coeff_p_mult_c_: algebra.
 313 *)
 314
 315 (* UNEXPORTED
 316 Hint Resolve nrCC3_a6: algebra.
 317 *)
 318
 319 inline cic:/CoRN/complex/NRootCC/nrCC3_a9.con.
 320
 321 inline cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con.
 322
 323 (* UNEXPORTED
 324 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
 325 *)
 326
 327 inline cic:/CoRN/complex/NRootCC/nrootCC_3_.con.
 328
 329 (* UNEXPORTED
 330 Hint Resolve nrootCC_3_: algebra.
 331 *)
 332
 333 (* UNEXPORTED
 334 Hint Resolve calculate_Im: algebra.
 335 *)
 336
 337 inline cic:/CoRN/complex/NRootCC/nrootCC_3.con.
 338
 339 (* UNEXPORTED
 340 Hint Resolve nrCC3_a2: algebra.
 341 *)
 342
 343 (* UNEXPORTED
 344 Hint Resolve nrCC3_a9: algebra.
 345 *)
 346
 347 inline cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con.
 348
 349 (* UNEXPORTED
 350 End NRootCC_3.
 351 *)
 352
 353 (* UNEXPORTED
 354 Section NRootCC_3'.
 355 *)
 356
 357 (*#*
 358 %\begin{convention}% Let [c:IR], [n:nat] and [n_:(lt (0) n)].
 359 %\end{convention}%
 360 *)
 361
 362 inline cic:/CoRN/complex/NRootCC/c.var.
 363
 364 inline cic:/CoRN/complex/NRootCC/n.var.
 365
 366 inline cic:/CoRN/complex/NRootCC/n_.var.
 367
 368 inline cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con.
 369
 370 inline cic:/CoRN/complex/NRootCC/nrootCC_3'.con.
 371
 372 inline cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con.
 373
 374 (* UNEXPORTED
 375 End NRootCC_3'.
 376 *)
 377
 378 (* UNEXPORTED
 379 Section NRootCC_4.
 380 *)
 381
 382 (* UNEXPORTED
 383 Section NRootCC_4_ap_real.
 384 *)
 385
 386 (*#*
 387 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)], [n : nat] and
 388 [n_:(odd n)]; define [c := a[+I*]b].
 389 %\end{convention}%
 390 *)
 391
 392 inline cic:/CoRN/complex/NRootCC/a.var.
 393
 394 inline cic:/CoRN/complex/NRootCC/b.var.
 395
 396 inline cic:/CoRN/complex/NRootCC/b_.var.
 397
 398 inline cic:/CoRN/complex/NRootCC/n.var.
 399
 400 inline cic:/CoRN/complex/NRootCC/n_.var.
 401
 402 (* begin hide *)
 403
 404 inline cic:/CoRN/complex/NRootCC/c.con.
 405
 406 (* end hide *)
 407
 408 (* UNEXPORTED
 409 Section NRootCC_4_solutions.
 410 *)
 411
 412 (* UNEXPORTED
 413 Hint Resolve nrootCC_3: algebra.
 414 *)
 415
 416 inline cic:/CoRN/complex/NRootCC/nrCC4_a1.con.
 417
 418 (*#*
 419 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
 420 %\end{convention}%
 421 *)
 422
 423 inline cic:/CoRN/complex/NRootCC/r2'.var.
 424
 425 inline cic:/CoRN/complex/NRootCC/c2.var.
 426
 427 inline cic:/CoRN/complex/NRootCC/r2'_.var.
 428
 429 (* UNEXPORTED
 430 Hint Resolve nrootCC_3': algebra.
 431 *)
 432
 433 inline cic:/CoRN/complex/NRootCC/nrCC4_a1'.con.
 434
 435 (* UNEXPORTED
 436 End NRootCC_4_solutions.
 437 *)
 438
 439 (* UNEXPORTED
 440 Section NRootCC_4_equations.
 441 *)
 442
 443 (*#*
 444 %\begin{convention}% Let [r,y2 : IR] be such that
 445 [(r[+I*]One) [^]n[*] (CC_conj c) [-] (r[+I*][--]One) [^]n[*]c [=] Zero]
 446 and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
 447 %\end{convention}%
 448 *)
 449
 450 inline cic:/CoRN/complex/NRootCC/r.var.
 451
 452 inline cic:/CoRN/complex/NRootCC/r_property.var.
 453
 454 inline cic:/CoRN/complex/NRootCC/y2.var.
 455
 456 inline cic:/CoRN/complex/NRootCC/y2_property.var.
 457
 458 inline cic:/CoRN/complex/NRootCC/nrCC4_a2.con.
 459
 460 inline cic:/CoRN/complex/NRootCC/nrCC4_a3.con.
 461
 462 inline cic:/CoRN/complex/NRootCC/nrCC4_a4.con.
 463
 464 inline cic:/CoRN/complex/NRootCC/nrCC4_y.con.
 465
 466 inline cic:/CoRN/complex/NRootCC/y.con.
 467
 468 inline cic:/CoRN/complex/NRootCC/nrCC4_x.con.
 469
 470 inline cic:/CoRN/complex/NRootCC/x.con.
 471
 472 inline cic:/CoRN/complex/NRootCC/nrCC4_a5.con.
 473
 474 inline cic:/CoRN/complex/NRootCC/nrCC4_a6.con.
 475
 476 inline cic:/CoRN/complex/NRootCC/nrCC4_z.con.
 477
 478 inline cic:/CoRN/complex/NRootCC/z.con.
 479
 480 inline cic:/CoRN/complex/NRootCC/nrCC4_a7.con.
 481
 482 (* UNEXPORTED
 483 Hint Resolve nrCC4_a6: algebra.
 484 *)
 485
 486 inline cic:/CoRN/complex/NRootCC/nrCC4_a8.con.
 487
 488 inline cic:/CoRN/complex/NRootCC/nrCC4_a9.con.
 489
 490 (* UNEXPORTED
 491 End NRootCC_4_equations.
 492 *)
 493
 494 inline cic:/CoRN/complex/NRootCC/nrCC4_a10.con.
 495
 496 inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con.
 497
 498 (* UNEXPORTED
 499 End NRootCC_4_ap_real.
 500 *)
 501
 502 (* UNEXPORTED
 503 Section NRootCC_4_ap_imag.
 504 *)
 505
 506 (*#*
 507 %\begin{convention}% Let [a,b : IR] and [n : nat] with [a [#] Zero]
 508 and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
 509 %\end{convention}%
 510 *)
 511
 512 inline cic:/CoRN/complex/NRootCC/a.var.
 513
 514 inline cic:/CoRN/complex/NRootCC/b.var.
 515
 516 inline cic:/CoRN/complex/NRootCC/a_.var.
 517
 518 inline cic:/CoRN/complex/NRootCC/n.var.
 519
 520 inline cic:/CoRN/complex/NRootCC/n_.var.
 521
 522 (* begin hide *)
 523
 524 inline cic:/CoRN/complex/NRootCC/c'.con.
 525
 526 inline cic:/CoRN/complex/NRootCC/a'.con.
 527
 528 inline cic:/CoRN/complex/NRootCC/b'.con.
 529
 530 (* end hide *)
 531
 532 inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con.
 533
 534 (* UNEXPORTED
 535 Hint Resolve nroot_minus_I_nexp: algebra.
 536 *)
 537
 538 inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con.
 539
 540 (* UNEXPORTED
 541 End NRootCC_4_ap_imag.
 542 *)
 543
 544 inline cic:/CoRN/complex/NRootCC/nrootCC_4.con.
 545
 546 (* UNEXPORTED
 547 End NRootCC_4.
 548 *)
 549
 550 (*#* Finally, the general definition of nth root. *)
 551
 552 (* UNEXPORTED
 553 Section NRootCC_5.
 554 *)
 555
 556 inline cic:/CoRN/complex/NRootCC/nrCC_5a2.con.
 557
 558 inline cic:/CoRN/complex/NRootCC/nrCC_5a3.con.
 559
 560 (* UNEXPORTED
 561 Hint Resolve nrCC_5a3: algebra.
 562 *)
 563
 564 (*#*
 565 %\begin{convention}% Let [c : CC] with [c [#] Zero].
 566 %\end{convention}%
 567 *)
 568
 569 inline cic:/CoRN/complex/NRootCC/c.var.
 570
 571 inline cic:/CoRN/complex/NRootCC/c_.var.
 572
 573 inline cic:/CoRN/complex/NRootCC/nrCC_5a4.con.
 574
 575 inline cic:/CoRN/complex/NRootCC/nrootCC_5.con.
 576
 577 (* UNEXPORTED
 578 End NRootCC_5.
 579 *)
 580
 581 (*#* Final definition *)
 582
 583 inline cic:/CoRN/complex/NRootCC/CnrootCC.con.
 584