X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fcomplex%2FNRootCC.ma;h=ff7b399568aef88454acacdee42f85eba0dce44b;hb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;hp=48688c5ee681a5bef147b38c0fc7c4178cfa3b41;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma index 48688c5ee..ff7b39956 100644 --- a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma +++ b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC". +include "CoRN_notation.ma". + (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *) (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *) @@ -26,17 +28,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC". (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *) -(* INCLUDE -CComplex -*) - -(* INCLUDE -Wf_nat -*) - -(* INCLUDE -ArithRing -*) +include "complex/CComplex.ma". (*#* * Roots of Complex Numbers @@ -47,9 +39,9 @@ Properties of non-zero complex numbers Section CC_ap_zero. *) -inline cic:/CoRN/complex/NRootCC/cc_ap_zero.con. +inline "cic:/CoRN/complex/NRootCC/cc_ap_zero.con". -inline cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con. +inline "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con". (* UNEXPORTED End CC_ap_zero. @@ -61,7 +53,7 @@ End CC_ap_zero. Section Imag_to_Real. *) -inline cic:/CoRN/complex/NRootCC/imag_to_real.con. +inline "cic:/CoRN/complex/NRootCC/imag_to_real.con". (* UNEXPORTED End Imag_to_Real. @@ -73,25 +65,25 @@ End Imag_to_Real. Section NRootI. *) -inline cic:/CoRN/complex/NRootCC/sqrt_Half.con. +inline "cic:/CoRN/complex/NRootCC/sqrt_Half.con". -inline cic:/CoRN/complex/NRootCC/sqrt_I.con. +inline "cic:/CoRN/complex/NRootCC/sqrt_I.con". -inline cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con. +inline "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con". -inline cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con. +inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con". -inline cic:/CoRN/complex/NRootCC/nroot_I.con. +inline "cic:/CoRN/complex/NRootCC/nroot_I.con". -inline cic:/CoRN/complex/NRootCC/nroot_I_nexp.con. +inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con". (* UNEXPORTED Hint Resolve nroot_I_nexp: algebra. *) -inline cic:/CoRN/complex/NRootCC/nroot_minus_I.con. +inline "cic:/CoRN/complex/NRootCC/nroot_minus_I.con". -inline cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con. +inline "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con". (* UNEXPORTED End NRootI. @@ -117,77 +109,77 @@ Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half], %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/a.var. +inline "cic:/CoRN/complex/NRootCC/a.var". -inline cic:/CoRN/complex/NRootCC/b.var. +inline "cic:/CoRN/complex/NRootCC/b.var". -inline cic:/CoRN/complex/NRootCC/b_.var. +inline "cic:/CoRN/complex/NRootCC/b_.var". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/c2.con. +inline "cic:/CoRN/complex/NRootCC/c2.con". (* end hide *) -inline cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/c.con. +inline "cic:/CoRN/complex/NRootCC/c.con". -inline cic:/CoRN/complex/NRootCC/a'2.con. +inline "cic:/CoRN/complex/NRootCC/a'2.con". (* end hide *) -inline cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/a'.con. +inline "cic:/CoRN/complex/NRootCC/a'.con". -inline cic:/CoRN/complex/NRootCC/b'2.con. +inline "cic:/CoRN/complex/NRootCC/b'2.con". (* end hide *) -inline cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/b'.con. +inline "cic:/CoRN/complex/NRootCC/b'.con". (* end hide *) -inline cic:/CoRN/complex/NRootCC/nrCC1_a3.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a3.con". -inline cic:/CoRN/complex/NRootCC/nrCC1_a4.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a4.con". (* UNEXPORTED Hint Resolve nrCC1_a4: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC1_a5.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a5.con". -inline cic:/CoRN/complex/NRootCC/nrCC1_a6.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a6.con". -inline cic:/CoRN/complex/NRootCC/nrCC1_a6'.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con". (* UNEXPORTED Hint Resolve nrCC1_a5: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con". -inline cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con. +inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con". (* UNEXPORTED Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con". (* UNEXPORTED End NRootCC_1_ap_real. @@ -206,19 +198,19 @@ Section NRootCC_1_ap_imag. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/a.var. +inline "cic:/CoRN/complex/NRootCC/a.var". -inline cic:/CoRN/complex/NRootCC/b.var. +inline "cic:/CoRN/complex/NRootCC/b.var". -inline cic:/CoRN/complex/NRootCC/a_.var. +inline "cic:/CoRN/complex/NRootCC/a_.var". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/c'.con. +inline "cic:/CoRN/complex/NRootCC/c'.con". -inline cic:/CoRN/complex/NRootCC/a'.con. +inline "cic:/CoRN/complex/NRootCC/a'.con". -inline cic:/CoRN/complex/NRootCC/b'.con. +inline "cic:/CoRN/complex/NRootCC/b'.con". (* end hide *) @@ -226,7 +218,7 @@ inline cic:/CoRN/complex/NRootCC/b'.con. Hint Resolve sqrt_I_nexp: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con". (* UNEXPORTED End NRootCC_1_ap_imag. @@ -234,7 +226,7 @@ End NRootCC_1_ap_imag. (*#* We now define the roots of arbitrary non zero complex numbers. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_1.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_1.con". (* UNEXPORTED End NRootCC_1. @@ -249,17 +241,17 @@ Section NRootCC_2. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/n.var. +inline "cic:/CoRN/complex/NRootCC/n.var". -inline cic:/CoRN/complex/NRootCC/c.var. +inline "cic:/CoRN/complex/NRootCC/c.var". -inline cic:/CoRN/complex/NRootCC/z.var. +inline "cic:/CoRN/complex/NRootCC/z.var". -inline cic:/CoRN/complex/NRootCC/c_.var. +inline "cic:/CoRN/complex/NRootCC/c_.var". -inline cic:/CoRN/complex/NRootCC/nrootCC_2'.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_2'.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_2.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_2.con". (* UNEXPORTED End NRootCC_2. @@ -269,44 +261,44 @@ End NRootCC_2. Section NRootCC_3. *) -inline cic:/CoRN/complex/NRootCC/Im_poly.con. +inline "cic:/CoRN/complex/NRootCC/Im_poly.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a1.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a1.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a2.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a2.con". (*#* %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat]. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/a.var. +inline "cic:/CoRN/complex/NRootCC/a.var". -inline cic:/CoRN/complex/NRootCC/b.var. +inline "cic:/CoRN/complex/NRootCC/b.var". -inline cic:/CoRN/complex/NRootCC/b_.var. +inline "cic:/CoRN/complex/NRootCC/b_.var". -inline cic:/CoRN/complex/NRootCC/n.var. +inline "cic:/CoRN/complex/NRootCC/n.var". -inline cic:/CoRN/complex/NRootCC/nrCC3_poly''.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a3.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a3.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a4.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a4.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a5.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a5.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a6.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a6.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_poly'.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con". (* UNEXPORTED Hint Resolve nrCC3_a3: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC3_a7.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a7.con". -inline cic:/CoRN/complex/NRootCC/nrCC3_a8.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a8.con". (* UNEXPORTED Hint Resolve nth_coeff_p_mult_c_: algebra. @@ -316,15 +308,15 @@ Hint Resolve nth_coeff_p_mult_c_: algebra. Hint Resolve nrCC3_a6: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC3_a9.con. +inline "cic:/CoRN/complex/NRootCC/nrCC3_a9.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con". (* UNEXPORTED Hint Resolve nrCC3_a1 nrCC3_a7: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_3_.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3_.con". (* UNEXPORTED Hint Resolve nrootCC_3_: algebra. @@ -334,7 +326,7 @@ Hint Resolve nrootCC_3_: algebra. Hint Resolve calculate_Im: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_3.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3.con". (* UNEXPORTED Hint Resolve nrCC3_a2: algebra. @@ -344,7 +336,7 @@ Hint Resolve nrCC3_a2: algebra. Hint Resolve nrCC3_a9: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con". (* UNEXPORTED End NRootCC_3. @@ -359,17 +351,17 @@ Section NRootCC_3'. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/c.var. +inline "cic:/CoRN/complex/NRootCC/c.var". -inline cic:/CoRN/complex/NRootCC/n.var. +inline "cic:/CoRN/complex/NRootCC/n.var". -inline cic:/CoRN/complex/NRootCC/n_.var. +inline "cic:/CoRN/complex/NRootCC/n_.var". -inline cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_3'.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3'.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con". (* UNEXPORTED End NRootCC_3'. @@ -389,19 +381,19 @@ Section NRootCC_4_ap_real. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/a.var. +inline "cic:/CoRN/complex/NRootCC/a.var". -inline cic:/CoRN/complex/NRootCC/b.var. +inline "cic:/CoRN/complex/NRootCC/b.var". -inline cic:/CoRN/complex/NRootCC/b_.var. +inline "cic:/CoRN/complex/NRootCC/b_.var". -inline cic:/CoRN/complex/NRootCC/n.var. +inline "cic:/CoRN/complex/NRootCC/n.var". -inline cic:/CoRN/complex/NRootCC/n_.var. +inline "cic:/CoRN/complex/NRootCC/n_.var". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/c.con. +inline "cic:/CoRN/complex/NRootCC/c.con". (* end hide *) @@ -413,24 +405,24 @@ Section NRootCC_4_solutions. Hint Resolve nrootCC_3: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC4_a1.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a1.con". (*#* %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)]. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/r2'.var. +inline "cic:/CoRN/complex/NRootCC/r2'.var". -inline cic:/CoRN/complex/NRootCC/c2.var. +inline "cic:/CoRN/complex/NRootCC/c2.var". -inline cic:/CoRN/complex/NRootCC/r2'_.var. +inline "cic:/CoRN/complex/NRootCC/r2'_.var". (* UNEXPORTED Hint Resolve nrootCC_3': algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC4_a1'.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con". (* UNEXPORTED End NRootCC_4_solutions. @@ -447,53 +439,53 @@ and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)]. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/r.var. +inline "cic:/CoRN/complex/NRootCC/r.var". -inline cic:/CoRN/complex/NRootCC/r_property.var. +inline "cic:/CoRN/complex/NRootCC/r_property.var". -inline cic:/CoRN/complex/NRootCC/y2.var. +inline "cic:/CoRN/complex/NRootCC/y2.var". -inline cic:/CoRN/complex/NRootCC/y2_property.var. +inline "cic:/CoRN/complex/NRootCC/y2_property.var". -inline cic:/CoRN/complex/NRootCC/nrCC4_a2.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a2.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a3.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a3.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a4.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a4.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_y.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_y.con". -inline cic:/CoRN/complex/NRootCC/y.con. +inline "cic:/CoRN/complex/NRootCC/y.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_x.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_x.con". -inline cic:/CoRN/complex/NRootCC/x.con. +inline "cic:/CoRN/complex/NRootCC/x.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a5.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a5.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a6.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a6.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_z.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_z.con". -inline cic:/CoRN/complex/NRootCC/z.con. +inline "cic:/CoRN/complex/NRootCC/z.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a7.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a7.con". (* UNEXPORTED Hint Resolve nrCC4_a6: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrCC4_a8.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a8.con". -inline cic:/CoRN/complex/NRootCC/nrCC4_a9.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a9.con". (* UNEXPORTED End NRootCC_4_equations. *) -inline cic:/CoRN/complex/NRootCC/nrCC4_a10.con. +inline "cic:/CoRN/complex/NRootCC/nrCC4_a10.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con". (* UNEXPORTED End NRootCC_4_ap_real. @@ -509,39 +501,39 @@ and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b']. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/a.var. +inline "cic:/CoRN/complex/NRootCC/a.var". -inline cic:/CoRN/complex/NRootCC/b.var. +inline "cic:/CoRN/complex/NRootCC/b.var". -inline cic:/CoRN/complex/NRootCC/a_.var. +inline "cic:/CoRN/complex/NRootCC/a_.var". -inline cic:/CoRN/complex/NRootCC/n.var. +inline "cic:/CoRN/complex/NRootCC/n.var". -inline cic:/CoRN/complex/NRootCC/n_.var. +inline "cic:/CoRN/complex/NRootCC/n_.var". (* begin hide *) -inline cic:/CoRN/complex/NRootCC/c'.con. +inline "cic:/CoRN/complex/NRootCC/c'.con". -inline cic:/CoRN/complex/NRootCC/a'.con. +inline "cic:/CoRN/complex/NRootCC/a'.con". -inline cic:/CoRN/complex/NRootCC/b'.con. +inline "cic:/CoRN/complex/NRootCC/b'.con". (* end hide *) -inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con". (* UNEXPORTED Hint Resolve nroot_minus_I_nexp: algebra. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con". (* UNEXPORTED End NRootCC_4_ap_imag. *) -inline cic:/CoRN/complex/NRootCC/nrootCC_4.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_4.con". (* UNEXPORTED End NRootCC_4. @@ -553,9 +545,9 @@ End NRootCC_4. Section NRootCC_5. *) -inline cic:/CoRN/complex/NRootCC/nrCC_5a2.con. +inline "cic:/CoRN/complex/NRootCC/nrCC_5a2.con". -inline cic:/CoRN/complex/NRootCC/nrCC_5a3.con. +inline "cic:/CoRN/complex/NRootCC/nrCC_5a3.con". (* UNEXPORTED Hint Resolve nrCC_5a3: algebra. @@ -566,13 +558,13 @@ Hint Resolve nrCC_5a3: algebra. %\end{convention}% *) -inline cic:/CoRN/complex/NRootCC/c.var. +inline "cic:/CoRN/complex/NRootCC/c.var". -inline cic:/CoRN/complex/NRootCC/c_.var. +inline "cic:/CoRN/complex/NRootCC/c_.var". -inline cic:/CoRN/complex/NRootCC/nrCC_5a4.con. +inline "cic:/CoRN/complex/NRootCC/nrCC_5a4.con". -inline cic:/CoRN/complex/NRootCC/nrootCC_5.con. +inline "cic:/CoRN/complex/NRootCC/nrootCC_5.con". (* UNEXPORTED End NRootCC_5. @@ -580,5 +572,5 @@ End NRootCC_5. (*#* Final definition *) -inline cic:/CoRN/complex/NRootCC/CnrootCC.con. +inline "cic:/CoRN/complex/NRootCC/CnrootCC.con".