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