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