diff options
Diffstat (limited to 'mathcomp/real_closed/complex.v')
| -rw-r--r-- | mathcomp/real_closed/complex.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/real_closed/complex.v b/mathcomp/real_closed/complex.v index ef32266..30b4b04 100644 --- a/mathcomp/real_closed/complex.v +++ b/mathcomp/real_closed/complex.v @@ -58,7 +58,7 @@ Section ComplexEqChoice. Variable R : Type. -Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [::a; b]. +Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [::a; b]. Definition complex_of_sqR (x : seq R) := if x is [:: a; b] then Some (a +i* b) else None. @@ -462,7 +462,7 @@ by rewrite -mulrA ['i%C * _]sqr_i mulrN1 opprB. Qed. Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0). -Proof. +Proof. rewrite realE; simpc; rewrite [0 == _]eq_sym. by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb). Qed. @@ -557,7 +557,7 @@ have F3: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) - a) / 2%:R. have F4: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) + a) / 2%:R. rewrite mulr_ge0 // -{2}[a]opprK subr_ge0 (ler_trans _ F2) //. by rewrite -(maxrN a) ler_maxr lerr orbT. -congr (_ +i* _); set u := if _ then _ else _. +congr (_ +i* _); set u := if _ then _ else _. rewrite mulrCA !mulrA. have->: (u * u) = 1. rewrite /u; case: (altP (_ =P _)); rewrite ?mul1r //. @@ -573,7 +573,7 @@ rewrite [_^+2 + _]addrC addrK -mulrA -expr2 sqrtrM ?exprn_even_ge0 //. rewrite !sqrtr_sqr -mulr_natr. rewrite [`|_^-1|]ger0_norm // -mulrA [_ * _%:R]mulrC divff //. rewrite mulr1 /u; case: (_ =P _)=>[->|]. - by rewrite normr0 mulr0. + by rewrite normr0 mulr0. by rewrite mulr_sg_norm. Qed. @@ -998,7 +998,7 @@ Qed. Lemma Lemma3 K d : Eigen1Vec K d -> forall r, CommonEigenVec K d r.+1. Proof. -move=> E1V_K_d; elim => [|r IHr m V]; first exact/Eigen1VecP. +move=> E1V_K_d; elim=> [|r IHr m V]; first exact/Eigen1VecP. move: (\rank V) {-2}V (leqnn (\rank V)) => n {V}. elim: n m => [|n IHn] m V. by rewrite leqn0 => /eqP ->; rewrite dvdn0. @@ -1111,7 +1111,7 @@ have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). case: n {x} (vec_mx x) => [//|n] x in HrV u v *. do ?[rewrite -(scalemxAl, scalemxAr, scalerN, scalerDr) |rewrite (mulmxN, mulNmx, trmxK, trmx_mul) - |rewrite ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=]. + |rewrite ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=]. congr (_ *: _). rewrite !(mulmxDr, mulmxDl, mulNmx, mulmxN, mulmxA, opprD, opprK). do ![move: (_ *m _ *m _)] => t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12. |