diff options
Diffstat (limited to 'mathcomp/attic/forms.v')
| -rw-r--r-- | mathcomp/attic/forms.v | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v index a1a987b..7098af9 100644 --- a/mathcomp/attic/forms.v +++ b/mathcomp/attic/forms.v @@ -20,7 +20,7 @@ Variable (R : fieldType). Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x . Lemma r2rv_morph_p : linear r2rv. -Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j;rewrite !mxE. Qed. +Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j; rewrite !mxE. Qed. Canonical Structure r2rv_morph := Linear r2rv_morph_p. @@ -28,8 +28,8 @@ Definition rv2r (A: 'rV[R]_1): R^o := A 0 0. Lemma r2rv_bij : bijective r2rv. Proof. -exists rv2r; first by move => x; rewrite /r2rv /rv2r /= mxE. -by move => x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=. +exists rv2r; first by move=> x; rewrite /r2rv /rv2r /= mxE. +by move=> x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=. Qed. Canonical Structure RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij. @@ -48,7 +48,7 @@ Variable (F : fieldType) (V : vectType F). Section SesquiLinearFormDef. Structure fautomorphism:= FautoMorph {fval :> F -> F; - _ : rmorphism fval; + _ : rmorphism fval; _ : bijective fval}. Variable theta: fautomorphism. @@ -72,7 +72,7 @@ Variable f : sesquilinear_form. Lemma bilin1 : forall x, {morph f x : y z / y + z}. Proof. by case f. Qed. Lemma bilin2 : forall x, {morph f ^~ x : y z / y + z}. Proof. by case f. Qed. Lemma bilina1 : forall a x y, f (a *: x) y = a * f x y. Proof. by case f. Qed. -Lemma bilina2 : forall a x y, f x (a *: y) = (theta a) * (f x y). +Lemma bilina2 : forall a x y, f x (a *: y) = (theta a) * (f x y). Proof. by case f. Qed. End SesquiLinearFormDef. @@ -97,9 +97,9 @@ Inductive symmetricf (f : sqlf): Prop := Lemma fsym_f0: forall (f: sqlf) x y, (symmetricf f) -> (f x y = 0 <-> f y x = 0). Proof. -move => f x y ;case; first by move=> [Htheta Hf];split; rewrite Hf. - by move=> [Htheta Hf];split; rewrite Hf; move/eqP;rewrite oppr_eq0; move/eqP->. -move=> Htheta;split; first by rewrite (Htheta y x) => ->; rewrite rmorph0. +move=> f x y; case; first by move=> [Htheta Hf]; split; rewrite Hf. + by move=> [Htheta Hf]; split; rewrite Hf; move/eqP; rewrite oppr_eq0; move/eqP->. +move=> Htheta; split; first by rewrite (Htheta y x) => ->; rewrite rmorph0. by rewrite (Htheta x y) => ->; rewrite rmorph0. Qed. @@ -114,21 +114,21 @@ Section orthogonal. Definition orthogonal x y := f x y = 0. Lemma ortho_sym: forall x y, orthogonal x y <-> orthogonal y x. -Proof. by move=> x y; apply:fsym_f0. Qed. +Proof. by move=> x y; apply: fsym_f0. Qed. Theorem Pythagore: forall u v, orthogonal u v -> f (u+v) (u+v) = f u u + f v v. Proof. -move => u v Huv; case:(ortho_sym u v ) => Hvu _. +move=> u v Huv; case: (ortho_sym u v ) => Hvu _. by rewrite !bilin1 !bilin2 Huv (Hvu Huv) add0r addr0. Qed. Lemma orthoD : forall u v w , orthogonal u v -> orthogonal u w -> orthogonal u (v + w). Proof. -by move => u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r. +by move=> u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r. Qed. Lemma orthoZ: forall u v a, orthogonal u v -> orthogonal (a *: u) v. -Proof. by move => u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed. +Proof. by move=> u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed. Variable x:V. @@ -139,7 +139,7 @@ Definition alpha_lfun := (lfun_of_fun alpha). Definition xbar := lker alpha_lfun . Lemma alpha_lin: linear alpha. -Proof. by move => a b c; rewrite /alpha bilin2 bilina1. Qed. +Proof. by move=> a b c; rewrite /alpha bilin2 bilina1. Qed. @@ -151,10 +151,10 @@ Qed. Lemma dim_xbar :forall vs,(\dim vs ) - 1 <= \dim (vs :&: xbar). -Proof. +Proof. move=> vs; rewrite -(addKn 1 (\dim (vs :&: xbar))) addnC leq_sub2r //. have H :\dim (alpha_lfun @: vs )<= 1 by rewrite -(dimR F) -dimvf dimvS // subvf. -by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))). +by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))). Qed. (* to be improved*) @@ -162,16 +162,16 @@ Lemma xbar_eqvs: forall vs, (forall v , v \in vs -> orthogonal v x )-> \dim (vs move=> vs Hvs. rewrite -(limg_ker_dim alpha_lfun vs). suff-> : \dim (alpha_lfun @: vs) = 0%nat by rewrite addn0. -apply/eqP; rewrite dimv_eq0; apply /vspaceP => w. -rewrite memv0;apply/memv_imgP. +apply/eqP; rewrite dimv_eq0; apply/vspaceP => w. +rewrite memv0; apply/memv_imgP. case e: (w==0). - exists 0; split ;first by rewrite mem0v. + exists 0; split; first by rewrite mem0v. apply sym_eq; rewrite (eqP e). rewrite (lfun_of_funK alpha_lin 0). rewrite /alpha_lfun /alpha /=. - by move:(bilina1 f 0 x x); rewrite scale0r mul0r. -move/eqP:e =>H2;case=> x0 [Hx0 Hw]. -apply H2;rewrite Hw;move: (Hvs x0 Hx0). + by move: (bilina1 f 0 x x); rewrite scale0r mul0r. +move/eqP:e =>H2; case=> x0 [Hx0 Hw]. +apply H2; rewrite Hw; move: (Hvs x0 Hx0). rewrite /orthogonal. by rewrite (lfun_of_funK alpha_lin x0). Qed. @@ -189,9 +189,9 @@ Import GRing.Theory. Lemma f2Q: forall x, Q x + Q x = f x x. Proof. -move=> x; apply:(@addrI _ (Q x + Q x)). +move=> x; apply: (@addrI _ (Q x + Q x)). rewrite !addrA -quadQ -[x + x](scaler_nat 2) quadQ. -by rewrite -mulrA !mulr_natl -addrA. +by rewrite -mulrA !mulr_natl -addrA. Qed. End LinearForm. |