From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.algebra.vector.html | 1101 +++++++++++++++-------------- 1 file changed, 552 insertions(+), 549 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.vector.html') diff --git a/docs/htmldoc/mathcomp.algebra.vector.html b/docs/htmldoc/mathcomp.algebra.vector.html index 7a5ac82..37872ef 100644 --- a/docs/htmldoc/mathcomp.algebra.vector.html +++ b/docs/htmldoc/mathcomp.algebra.vector.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -146,48 +145,48 @@ Variable R : ringType.

-Definition axiom_def n (V : lmodType R) of phant V :=
-  {v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
+Definition axiom_def n (V : lmodType R) of phant V :=
+  {v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.

-Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
+Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).

Structure class_of V := Class {
  base : GRing.Lmodule.class_of R V;
-  mixin : mixin_of (GRing.Lmodule.Pack _ base V)
+  mixin : mixin_of (GRing.Lmodule.Pack _ base)
}.

-Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
-Variables (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone c of phant_id class c := @Pack phR T c T.
-Let xT := let: Pack T _ _ := cT in T.
-Notation xclass := (class : class_of xT).
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
+Variables (phR : phant R) (T : Type) (cT : type phR).
+Definition class := let: Pack _ c := cT return class_of cT in c.
+Definition clone c of phant_id class c := @Pack phR T c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition dim := let: Mixin n _ := mixin class in n.

-Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0 T)) :=
-  fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack phR (@Class T b m) T.
+Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) :=
+  fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
+  fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).

-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.

End ClassDef.
-Notation axiom n V := (axiom_def n (Phant V)).
+Notation axiom n V := (axiom_def n (Phant V)).

Section OtherDefs.
-Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
-  Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
-Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
-  Hom of 'M[R]_(vT, wT).
+Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
+  Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
+Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
+  Hom of 'M[R]_(vT, wT).
End OtherDefs.

@@ -205,19 +204,19 @@ Canonical zmodType.
Coercion lmodType: type>-> GRing.Lmodule.type.
Canonical lmodType.
-Notation vectType R := (@type _ (Phant R)).
+Notation vectType R := (@type _ (Phant R)).
Notation VectType R V mV :=
-   (@pack _ (Phant R) V _ mV _ _ id _ id).
+   (@pack _ (Phant R) V _ mV _ _ id _ id).
Notation VectMixin := Mixin.
-Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
+Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
+Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
  (at level 0, format "[ 'vectType' R 'of' T ]") : form_scope.

-Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
-Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
-Notation "''End' ( vT )" := (hom vT vT) : type_scope.
+Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
+Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
+Notation "''End' ( vT )" := (hom vT vT) : type_scope.

@@ -247,18 +246,18 @@ Definition v2r := s2val v2r_subproof.

-Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
-Fact r2v_subproof : {r2v | cancel r2v v2r}.
+Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
+Fact r2v_subproof : {r2v | cancel r2v v2r}.
Definition r2v := sval r2v_subproof.

-Lemma r2vK : cancel r2v v2r.
-Lemma r2v_inj : injective r2v.
-Lemma v2rK : cancel v2r r2v.
-Lemma v2r_inj : injective v2r.
+Lemma r2vK : cancel r2v v2r.
+Lemma r2v_inj : injective r2v.
+Lemma v2rK : cancel v2r r2v.
+Lemma v2r_inj : injective v2r.

-Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
+Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
Canonical r2v_linear := Linear (can2_linear v2rK r2vK).
End Iso.
@@ -267,28 +266,28 @@ Variables (K : fieldType) (vT : vectType K).

-Definition b2mx n (X : n.-tuple vT) := \matrix_i v2r (tnth X i).
-Lemma b2mxK n (X : n.-tuple vT) i : r2v (row i (b2mx X)) = X`_i.
+Definition b2mx n (X : n.-tuple vT) := \matrix_i v2r (tnth X i).
+Lemma b2mxK n (X : n.-tuple vT) i : r2v (row i (b2mx X)) = X`_i.

Definition vs2mx {phV} (U : @space K vT phV) := let: Space mx _ := U in mx.
-Lemma gen_vs2mx (U : {vspace vT}) : <<vs2mx U>>%MS = vs2mx U.
+Lemma gen_vs2mx (U : {vspace vT}) : <<vs2mx U>>%MS = vs2mx U.

-Fact mx2vs_subproof m (A : 'M[K]_(m, vT)) : <<(<<A>>)>>%MS == <<A>>%MS.
- Definition mx2vs {m} A : {vspace vT} := Space _ (@mx2vs_subproof m A).
+Fact mx2vs_subproof m (A : 'M[K]_(m, vT)) : <<(<<A>>)>>%MS == <<A>>%MS.
+ Definition mx2vs {m} A : {vspace vT} := Space _ (@mx2vs_subproof m A).

-Canonical space_subType := [subType for @vs2mx (Phant vT)].
-Lemma vs2mxK : cancel vs2mx mx2vs.
- Lemma mx2vsK m (M : 'M_(m, vT)) : (vs2mx (mx2vs M) :=: M)%MS.
+Canonical space_subType := [subType for @vs2mx (Phant vT)].
+Lemma vs2mxK : cancel vs2mx mx2vs.
+ Lemma mx2vsK m (M : 'M_(m, vT)) : (vs2mx (mx2vs M) :=: M)%MS.
End Vspace.

Section Hom.
Variables (R : ringType) (aT rT : vectType R).
-Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
-Canonical hom_subType := [newType for f2mx].
+Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
+Canonical hom_subType := [newType for f2mx].
End Hom.

@@ -306,17 +305,17 @@
Variables (K : fieldType) (vT : vectType K).
-Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).
+Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).

-Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT} by <:].
-Canonical space_eqType := EqType {vspace vT} space_eqMixin.
-Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT} by <:].
-Canonical space_choiceType := ChoiceType {vspace vT} space_choiceMixin.
+Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT} by <:].
+Canonical space_eqType := EqType {vspace vT} space_eqMixin.
+Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT} by <:].
+Canonical space_choiceType := ChoiceType {vspace vT} space_choiceMixin.

-Definition dimv U := \rank (vs2mx U).
-Definition subsetv U V := (vs2mx U ≤ vs2mx V)%MS.
+Definition dimv U := \rank (vs2mx U).
+Definition subsetv U V := (vs2mx U ≤ vs2mx V)%MS.
Definition vline u := mx2vs (v2r u).

@@ -326,26 +325,26 @@ Vspace membership is defined as line inclusion.
-Definition pred_of_vspace phV (U : Vector.space phV) : pred_class :=
-  fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
+Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT} :=
+  fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
Canonical vspace_predType :=
-  @mkPredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
+  @PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).

-Definition fullv : {vspace vT} := mx2vs 1%:M.
-Definition addv U V := mx2vs (vs2mx U + vs2mx V).
-Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
-Definition complv U := mx2vs (vs2mx U)^C.
-Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
+Definition fullv : {vspace vT} := mx2vs 1%:M.
+Definition addv U V := mx2vs (vs2mx U + vs2mx V).
+Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
+Definition complv U := mx2vs (vs2mx U)^C.
+Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
Definition vpick U := r2v (nz_row (vs2mx U)).
-Fact span_key : unit.
+Fact span_key : unit.
Definition span_expanded_def X := mx2vs (b2mx (in_tuple X)).
-Definition span := locked_with span_key span_expanded_def.
-Canonical span_unlockable := [unlockable fun span].
+Definition span := locked_with span_key span_expanded_def.
+Canonical span_unlockable := [unlockable fun span].
Definition vbasis_def U :=
-  [tuple r2v (row i (row_base (vs2mx U))) | i < dimv U].
-Definition vbasis := locked_with span_key vbasis_def.
-Canonical vbasis_unlockable := [unlockable fun vbasis].
+  [tuple r2v (row i (row_base (vs2mx U))) | i < dimv U].
+Definition vbasis := locked_with span_key vbasis_def.
+Canonical vbasis_unlockable := [unlockable fun vbasis].

@@ -356,100 +355,100 @@

-Definition free X := dimv (span X) == size X.
-Definition basis_of U X := (span X == U) && free X.
+Definition free X := dimv (span X) == size X.
+Definition basis_of U X := (span X == U) && free X.

End VspaceDefs.

-Coercion pred_of_vspace : Vector.space >-> pred_class.
-Notation "\dim U" := (dimv U) : nat_scope.
-Notation "U <= V" := (subsetv U V) : vspace_scope.
-Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
-Notation "<[ v ] >" := (vline v) : vspace_scope.
-Notation "<< X >>" := (span X) : vspace_scope.
-Notation "0" := (vline 0) : vspace_scope.
- -
-Notation "U + V" := (addv U V) : vspace_scope.
-Notation "U :&: V" := (capv U V) : vspace_scope.
-Notation "U ^C" := (complv U) (at level 8, format "U ^C") : vspace_scope.
-Notation "U :\: V" := (diffv U V) : vspace_scope.
-Notation "{ : vT }" := (@fullv _ vT) (only parsing) : vspace_scope.
- -
-Notation "\sum_ ( i <- r | P ) U" :=
-  (\big[addv/0%VS]_(i <- r | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i <- r ) U" :=
-  (\big[addv/0%VS]_(i <- r) U%VS) : vspace_scope.
-Notation "\sum_ ( m <= i < n | P ) U" :=
-  (\big[addv/0%VS]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( m <= i < n ) U" :=
-  (\big[addv/0%VS]_(m ≤ i < n) U%VS) : vspace_scope.
-Notation "\sum_ ( i | P ) U" :=
-  (\big[addv/0%VS]_(i | P%B) U%VS) : vspace_scope.
-Notation "\sum_ i U" :=
-  (\big[addv/0%VS]_i U%VS) : vspace_scope.
-Notation "\sum_ ( i : t | P ) U" :=
-  (\big[addv/0%VS]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
-Notation "\sum_ ( i : t ) U" :=
-  (\big[addv/0%VS]_(i : t) U%VS) (only parsing) : vspace_scope.
-Notation "\sum_ ( i < n | P ) U" :=
-  (\big[addv/0%VS]_(i < n | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i < n ) U" :=
-  (\big[addv/0%VS]_(i < n) U%VS) : vspace_scope.
-Notation "\sum_ ( i 'in' A | P ) U" :=
-  (\big[addv/0%VS]_(i in A | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i 'in' A ) U" :=
-  (\big[addv/0%VS]_(i in A) U%VS) : vspace_scope.
- -
-Notation "\bigcap_ ( i <- r | P ) U" :=
-  (\big[capv/fullv]_(i <- r | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i <- r ) U" :=
-  (\big[capv/fullv]_(i <- r) U%VS) : vspace_scope.
-Notation "\bigcap_ ( m <= i < n | P ) U" :=
-  (\big[capv/fullv]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( m <= i < n ) U" :=
-  (\big[capv/fullv]_(m ≤ i < n) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i | P ) U" :=
-  (\big[capv/fullv]_(i | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ i U" :=
-  (\big[capv/fullv]_i U%VS) : vspace_scope.
-Notation "\bigcap_ ( i : t | P ) U" :=
-  (\big[capv/fullv]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
-Notation "\bigcap_ ( i : t ) U" :=
-  (\big[capv/fullv]_(i : t) U%VS) (only parsing) : vspace_scope.
-Notation "\bigcap_ ( i < n | P ) U" :=
-  (\big[capv/fullv]_(i < n | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i < n ) U" :=
-  (\big[capv/fullv]_(i < n) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i 'in' A | P ) U" :=
-  (\big[capv/fullv]_(i in A | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i 'in' A ) U" :=
-  (\big[capv/fullv]_(i in A) U%VS) : vspace_scope.
+Coercion pred_of_vspace : Vector.space >-> pred_sort.
+Notation "\dim U" := (dimv U) : nat_scope.
+Notation "U <= V" := (subsetv U V) : vspace_scope.
+Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
+Notation "<[ v ] >" := (vline v) : vspace_scope.
+Notation "<< X >>" := (span X) : vspace_scope.
+Notation "0" := (vline 0) : vspace_scope.
+ +
+Notation "U + V" := (addv U V) : vspace_scope.
+Notation "U :&: V" := (capv U V) : vspace_scope.
+Notation "U ^C" := (complv U) (at level 8, format "U ^C") : vspace_scope.
+Notation "U :\: V" := (diffv U V) : vspace_scope.
+Notation "{ : vT }" := (@fullv _ vT) (only parsing) : vspace_scope.
+ +
+Notation "\sum_ ( i <- r | P ) U" :=
+  (\big[addv/0%VS]_(i <- r | P%B) U%VS) : vspace_scope.
+Notation "\sum_ ( i <- r ) U" :=
+  (\big[addv/0%VS]_(i <- r) U%VS) : vspace_scope.
+Notation "\sum_ ( m <= i < n | P ) U" :=
+  (\big[addv/0%VS]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
+Notation "\sum_ ( m <= i < n ) U" :=
+  (\big[addv/0%VS]_(m ≤ i < n) U%VS) : vspace_scope.
+Notation "\sum_ ( i | P ) U" :=
+  (\big[addv/0%VS]_(i | P%B) U%VS) : vspace_scope.
+Notation "\sum_ i U" :=
+  (\big[addv/0%VS]_i U%VS) : vspace_scope.
+Notation "\sum_ ( i : t | P ) U" :=
+  (\big[addv/0%VS]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
+Notation "\sum_ ( i : t ) U" :=
+  (\big[addv/0%VS]_(i : t) U%VS) (only parsing) : vspace_scope.
+Notation "\sum_ ( i < n | P ) U" :=
+  (\big[addv/0%VS]_(i < n | P%B) U%VS) : vspace_scope.
+Notation "\sum_ ( i < n ) U" :=
+  (\big[addv/0%VS]_(i < n) U%VS) : vspace_scope.
+Notation "\sum_ ( i 'in' A | P ) U" :=
+  (\big[addv/0%VS]_(i in A | P%B) U%VS) : vspace_scope.
+Notation "\sum_ ( i 'in' A ) U" :=
+  (\big[addv/0%VS]_(i in A) U%VS) : vspace_scope.
+ +
+Notation "\bigcap_ ( i <- r | P ) U" :=
+  (\big[capv/fullv]_(i <- r | P%B) U%VS) : vspace_scope.
+Notation "\bigcap_ ( i <- r ) U" :=
+  (\big[capv/fullv]_(i <- r) U%VS) : vspace_scope.
+Notation "\bigcap_ ( m <= i < n | P ) U" :=
+  (\big[capv/fullv]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
+Notation "\bigcap_ ( m <= i < n ) U" :=
+  (\big[capv/fullv]_(m ≤ i < n) U%VS) : vspace_scope.
+Notation "\bigcap_ ( i | P ) U" :=
+  (\big[capv/fullv]_(i | P%B) U%VS) : vspace_scope.
+Notation "\bigcap_ i U" :=
+  (\big[capv/fullv]_i U%VS) : vspace_scope.
+Notation "\bigcap_ ( i : t | P ) U" :=
+  (\big[capv/fullv]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
+Notation "\bigcap_ ( i : t ) U" :=
+  (\big[capv/fullv]_(i : t) U%VS) (only parsing) : vspace_scope.
+Notation "\bigcap_ ( i < n | P ) U" :=
+  (\big[capv/fullv]_(i < n | P%B) U%VS) : vspace_scope.
+Notation "\bigcap_ ( i < n ) U" :=
+  (\big[capv/fullv]_(i < n) U%VS) : vspace_scope.
+Notation "\bigcap_ ( i 'in' A | P ) U" :=
+  (\big[capv/fullv]_(i in A | P%B) U%VS) : vspace_scope.
+Notation "\bigcap_ ( i 'in' A ) U" :=
+  (\big[capv/fullv]_(i in A) U%VS) : vspace_scope.

Section VectorTheory.

Variables (K : fieldType) (vT : vectType K).
-Implicit Types (a : K) (u v w : vT) (X Y : seq vT) (U V W : {vspace vT}).
+Implicit Types (a : K) (u v w : vT) (X Y : seq vT) (U V W : {vspace vT}).



-Fact vspace_key U : pred_key U.
-Canonical vspace_keyed U := KeyedPred (vspace_key U).
+Fact vspace_key U : pred_key U.
+Canonical vspace_keyed U := KeyedPred (vspace_key U).

-Lemma memvE v U : (v \in U) = (<[v]> ≤ U)%VS.
+Lemma memvE v U : (v \in U) = (<[v]> ≤ U)%VS.

-Lemma vlineP v1 v2 : reflect (∃ k, v1 = k *: v2) (v1 \in <[v2]>)%VS.
+Lemma vlineP v1 v2 : reflect (∃ k, v1 = k *: v2) (v1 \in <[v2]>)%VS.

Fact memv_submod_closed U : submod_closed U.
@@ -459,40 +458,40 @@ Canonical memv_submodPred U := SubmodPred (memv_submod_closed U).

-Lemma mem0v U : 0 \in U.
-Lemma memvN U v : (- v \in U) = (v \in U).
-Lemma memvD U : {in U &, ∀ u v, u + v \in U}.
-Lemma memvB U : {in U &, ∀ u v, u - v \in U}.
-Lemma memvZ U k : {in U, ∀ v, k *: v \in U}.
+Lemma mem0v U : 0 \in U.
+Lemma memvN U v : (- v \in U) = (v \in U).
+Lemma memvD U : {in U &, ∀ u v, u + v \in U}.
+Lemma memvB U : {in U &, ∀ u v, u - v \in U}.
+Lemma memvZ U k : {in U, ∀ v, k *: v \in U}.

-Lemma memv_suml I r (P : pred I) vs U :
-  (∀ i, P i → vs i \in U) → \sum_(i <- r | P i) vs i \in U.
+Lemma memv_suml I r (P : pred I) vs U :
+  (∀ i, P i → vs i \in U) → \sum_(i <- r | P i) vs i \in U.

-Lemma memv_line u : u \in <[u]>%VS.
+Lemma memv_line u : u \in <[u]>%VS.

-Lemma subvP U V : reflect {subset U ≤ V} (U ≤ V)%VS.
+Lemma subvP U V : reflect {subset U ≤ V} (U ≤ V)%VS.

-Lemma subvv U : (U ≤ U)%VS.
-Hint Resolve subvv.
+Lemma subvv U : (U ≤ U)%VS.
+Hint Resolve subvv : core.

-Lemma subv_trans : transitive subV.
+Lemma subv_trans : transitive subV.

-Lemma subv_anti : antisymmetric subV.
+Lemma subv_anti : antisymmetric subV.

-Lemma eqEsubv U V : (U == V) = (U ≤ V ≤ U)%VS.
+Lemma eqEsubv U V : (U == V) = (U ≤ V ≤ U)%VS.

-Lemma vspaceP U V : U =i V ↔ U = V.
+Lemma vspaceP U V : U =i V ↔ U = V.

-Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U ≤ V)%VS).
+Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U ≤ V)%VS).

@@ -501,13 +500,13 @@ Empty space.
-Lemma sub0v U : (0 ≤ U)%VS.
+Lemma sub0v U : (0 ≤ U)%VS.

-Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).
+Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).

-Lemma memv0 v : v \in 0%VS = (v == 0).
+Lemma memv0 v : v \in 0%VS = (v == 0).

@@ -518,8 +517,8 @@

-Lemma subvf U : (U ≤ fullv)%VS.
-Lemma memvf v : v \in fullv.
+Lemma subvf U : (U ≤ fullv)%VS.
+Lemma memvf v : v \in fullv.

@@ -528,10 +527,10 @@ Picking a non-zero vector in a subspace.
-Lemma memv_pick U : vpick U \in U.
+Lemma memv_pick U : vpick U \in U.

-Lemma vpick0 U : (vpick U == 0) = (U == 0%VS).
+Lemma vpick0 U : (vpick U == 0) = (U == 0%VS).

@@ -540,79 +539,79 @@ Sum of subspaces.
-Lemma subv_add U V W : (U + V ≤ W)%VS = (U ≤ W)%VS && (V ≤ W)%VS.
+Lemma subv_add U V W : (U + V ≤ W)%VS = (U ≤ W)%VS && (V ≤ W)%VS.

-Lemma addvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 + V1 ≤ U2 + V2)%VS.
+Lemma addvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 + V1 ≤ U2 + V2)%VS.

-Lemma addvSl U V : (U ≤ U + V)%VS.
+Lemma addvSl U V : (U ≤ U + V)%VS.

-Lemma addvSr U V : (V ≤ U + V)%VS.
+Lemma addvSr U V : (V ≤ U + V)%VS.

-Lemma addvC : commutative addV.
+Lemma addvC : commutative addV.

-Lemma addvA : associative addV.
+Lemma addvA : associative addV.

-Lemma addv_idPl {U V}: reflect (U + V = U)%VS (V ≤ U)%VS.
+Lemma addv_idPl {U V}: reflect (U + V = U)%VS (V ≤ U)%VS.

-Lemma addv_idPr {U V} : reflect (U + V = V)%VS (U ≤ V)%VS.
+Lemma addv_idPr {U V} : reflect (U + V = V)%VS (U ≤ V)%VS.

-Lemma addvv : idempotent addV.
+Lemma addvv : idempotent addV.

-Lemma add0v : left_id 0%VS addV.
+Lemma add0v : left_id 0%VS addV.

-Lemma addv0 : right_id 0%VS addV.
+Lemma addv0 : right_id 0%VS addV.

-Lemma sumfv : left_zero fullv addV.
+Lemma sumfv : left_zero fullv addV.

-Lemma addvf : right_zero fullv addV.
+Lemma addvf : right_zero fullv addV.

Canonical addv_monoid := Monoid.Law addvA add0v addv0.
Canonical addv_comoid := Monoid.ComLaw addvC.

-Lemma memv_add u v U V : u \in U → v \in V → u + v \in (U + V)%VS.
+Lemma memv_add u v U V : u \in U → v \in V → u + v \in (U + V)%VS.

Lemma memv_addP {w U V} :
-  reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
-          (w \in U + V)%VS.
+  reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
+          (w \in U + V)%VS.

Section BigSum.
Variable I : finType.
-Implicit Type P : pred I.
+Implicit Type P : pred I.

Lemma sumv_sup i0 P U Vs :
-  P i0 → (U ≤ Vs i0)%VS → (U ≤ \sum_(i | P i) Vs i)%VS.
+  P i0 → (U ≤ Vs i0)%VS → (U ≤ \sum_(i | P i) Vs i)%VS.

Lemma subv_sumP {P Us V} :
-  reflect (∀ i, P i → Us i ≤ V)%VS (\sum_(i | P i) Us i ≤ V)%VS.
+  reflect (∀ i, P i → Us i ≤ V)%VS (\sum_(i | P i) Us i ≤ V)%VS.

-Lemma memv_sumr P vs (Us : I → {vspace vT}) :
-    (∀ i, P i → vs i \in Us i) →
-  \sum_(i | P i) vs i \in (\sum_(i | P i) Us i)%VS.
+Lemma memv_sumr P vs (Us : I → {vspace vT}) :
+    (∀ i, P i → vs i \in Us i) →
+  \sum_(i | P i) vs i \in (\sum_(i | P i) Us i)%VS.

-Lemma memv_sumP {P} {Us : I → {vspace vT}} {v} :
-  reflect (exists2 vs, ∀ i, P i → vs i \in Us i
-                     & v = \sum_(i | P i) vs i)
-          (v \in \sum_(i | P i) Us i)%VS.
+Lemma memv_sumP {P} {Us : I → {vspace vT}} {v} :
+  reflect (exists2 vs, ∀ i, P i → vs i \in Us i
+                     & v = \sum_(i | P i) vs i)
+          (v \in \sum_(i | P i) Us i)%VS.

End BigSum.
@@ -626,72 +625,72 @@

-Lemma subv_cap U V W : (U ≤ V :&: W)%VS = (U ≤ V)%VS && (U ≤ W)%VS.
+Lemma subv_cap U V W : (U ≤ V :&: W)%VS = (U ≤ V)%VS && (U ≤ W)%VS.

-Lemma capvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 :&: V1 ≤ U2 :&: V2)%VS.
+Lemma capvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 :&: V1 ≤ U2 :&: V2)%VS.

-Lemma capvSl U V : (U :&: V ≤ U)%VS.
+Lemma capvSl U V : (U :&: V ≤ U)%VS.

-Lemma capvSr U V : (U :&: V ≤ V)%VS.
+Lemma capvSr U V : (U :&: V ≤ V)%VS.

-Lemma capvC : commutative capV.
+Lemma capvC : commutative capV.

-Lemma capvA : associative capV.
+Lemma capvA : associative capV.

-Lemma capv_idPl {U V} : reflect (U :&: V = U)%VS (U ≤ V)%VS.
+Lemma capv_idPl {U V} : reflect (U :&: V = U)%VS (U ≤ V)%VS.

-Lemma capv_idPr {U V} : reflect (U :&: V = V)%VS (V ≤ U)%VS.
+Lemma capv_idPr {U V} : reflect (U :&: V = V)%VS (V ≤ U)%VS.

-Lemma capvv : idempotent capV.
+Lemma capvv : idempotent capV.

-Lemma cap0v : left_zero 0%VS capV.
+Lemma cap0v : left_zero 0%VS capV.

-Lemma capv0 : right_zero 0%VS capV.
+Lemma capv0 : right_zero 0%VS capV.

-Lemma capfv : left_id fullv capV.
+Lemma capfv : left_id fullv capV.

-Lemma capvf : right_id fullv capV.
+Lemma capvf : right_id fullv capV.

Canonical capv_monoid := Monoid.Law capvA capfv capvf.
Canonical capv_comoid := Monoid.ComLaw capvC.

-Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).
+Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).

-Lemma memv_capP {w U V} : reflect (w \in U ∧ w \in V) (w \in U :&: V)%VS.
+Lemma memv_capP {w U V} : reflect (w \in U ∧ w \in V) (w \in U :&: V)%VS.

-Lemma vspace_modl U V W : (U ≤ W → U + (V :&: W) = (U + V) :&: W)%VS.
+Lemma vspace_modl U V W : (U ≤ W → U + (V :&: W) = (U + V) :&: W)%VS.

-Lemma vspace_modr U V W : (W ≤ U → (U :&: V) + W = U :&: (V + W))%VS.
+Lemma vspace_modr U V W : (W ≤ U → (U :&: V) + W = U :&: (V + W))%VS.

Section BigCap.
Variable I : finType.
-Implicit Type P : pred I.
+Implicit Type P : pred I.

Lemma bigcapv_inf i0 P Us V :
-  P i0 → (Us i0 ≤ V → \bigcap_(i | P i) Us i ≤ V)%VS.
+  P i0 → (Us i0 ≤ V → \bigcap_(i | P i) Us i ≤ V)%VS.

Lemma subv_bigcapP {P U Vs} :
-  reflect (∀ i, P i → U ≤ Vs i)%VS (U ≤ \bigcap_(i | P i) Vs i)%VS.
+  reflect (∀ i, P i → U ≤ Vs i)%VS (U ≤ \bigcap_(i | P i) Vs i)%VS.

End BigCap.
@@ -703,10 +702,10 @@ Complement
-Lemma addv_complf U : (U + U^C)%VS = fullv.
+Lemma addv_complf U : (U + U^C)%VS = fullv.

-Lemma capv_compl U : (U :&: U^C = 0)%VS.
+Lemma capv_compl U : (U :&: U^C = 0)%VS.

@@ -715,16 +714,16 @@ Difference
-Lemma diffvSl U V : (U :\: V ≤ U)%VS.
+Lemma diffvSl U V : (U :\: V ≤ U)%VS.

-Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.
+Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.

-Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.
+Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.

-Lemma addv_diff U V : (U :\: V + V = U + V)%VS.
+Lemma addv_diff U V : (U :\: V + V = U + V)%VS.

@@ -733,52 +732,52 @@ Subspace dimension.
-Lemma dimv0 : \dim (0%VS : {vspace vT}) = 0%N.
+Lemma dimv0 : \dim (0%VS : {vspace vT}) = 0%N.

-Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).
+Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).

-Lemma dimvf : \dim {:vT} = Vector.dim vT.
+Lemma dimvf : \dim {:vT} = Vector.dim vT.

-Lemma dim_vline v : \dim <[v]> = (v != 0).
+Lemma dim_vline v : \dim <[v]> = (v != 0).

-Lemma dimvS U V : (U ≤ V)%VS → \dim U ≤ \dim V.
+Lemma dimvS U V : (U ≤ V)%VS → \dim U ≤ \dim V.

-Lemma dimv_leqif_sup U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (V ≤ U)%VS.
+Lemma dimv_leqif_sup U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (V ≤ U)%VS.

-Lemma dimv_leqif_eq U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (U == V).
+Lemma dimv_leqif_eq U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (U == V).

-Lemma eqEdim U V : (U == V) = (U ≤ V)%VS && (\dim V ≤ \dim U).
+Lemma eqEdim U V : (U == V) = (U ≤ V)%VS && (\dim V ≤ \dim U).

-Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.
+Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.

-Lemma dimv_cap_compl U V : (\dim (U :&: V) + \dim (U :\: V))%N = \dim U.
+Lemma dimv_cap_compl U V : (\dim (U :&: V) + \dim (U :\: V))%N = \dim U.

-Lemma dimv_sum_cap U V : (\dim (U + V) + \dim (U :&: V) = \dim U + \dim V)%N.
+Lemma dimv_sum_cap U V : (\dim (U + V) + \dim (U :&: V) = \dim U + \dim V)%N.

Lemma dimv_disjoint_sum U V :
-  (U :&: V = 0)%VS → \dim (U + V) = (\dim U + \dim V)%N.
+  (U :&: V = 0)%VS → \dim (U + V) = (\dim U + \dim V)%N.

Lemma dimv_add_leqif U V :
-  \dim (U + V) ≤ \dim U + \dim V ?= iff (U :&: V ≤ 0)%VS.
+  \dim (U + V) ≤ \dim U + \dim V ?= iff (U :&: V ≤ 0)%VS.

-Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U ≤ V)%VS.
+Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U ≤ V)%VS.

-Lemma dimv_leq_sum I r (P : pred I) (Us : I → {vspace vT}) :
-  \dim (\sum_(i <- r | P i) Us i) ≤ \sum_(i <- r | P i) \dim (Us i).
+Lemma dimv_leq_sum I r (P : pred I) (Us : I → {vspace vT}) :
+  \dim (\sum_(i <- r | P i) Us i) ≤ \sum_(i <- r | P i) \dim (Us i).

Section SumExpr.
@@ -793,9 +792,9 @@
Structure addv_expr := Sumv {
-  addv_val :> wrapped {vspace vT};
-  addv_dim : wrapped nat;
-  _ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
+  addv_val :> wrapped {vspace vT};
+  addv_dim : wrapped nat;
+  _ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
}.

@@ -806,16 +805,16 @@
Definition vs2mx_sum_expr_subproof (S : addv_expr) :
-  mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
+  mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
Canonical vs2mx_sum_expr S := ProperMxsumExpr (vs2mx_sum_expr_subproof S).

-Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).
+Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).

Structure proper_addv_expr := ProperSumvExpr {
-  proper_addv_val :> {vspace vT};
-  proper_addv_dim :> nat;
+  proper_addv_val :> {vspace vT};
+  proper_addv_dim :> nat;
  _ : mxsum_spec (vs2mx proper_addv_val) proper_addv_dim
}.
@@ -825,29 +824,29 @@
Canonical proper_addv (S : proper_addv_expr) :=
-  @Sumv (wrap (S : {vspace vT})) (wrap (S : nat)) (proper_addvP S).
+  @Sumv (wrap (S : {vspace vT})) (wrap (S : nat)) (proper_addvP S).

Section Binary.
Variables S1 S2 : addv_expr.
Fact binary_addv_subproof :
-  mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
-             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
+  mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
+             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Canonical binary_addv_expr := ProperSumvExpr binary_addv_subproof.
End Binary.

Section Nary.
-Variables (I : Type) (r : seq I) (P : pred I) (S_ : I → addv_expr).
+Variables (I : Type) (r : seq I) (P : pred I) (S_ : I → addv_expr).
Fact nary_addv_subproof :
-  mxsum_spec (vs2mx (\sum_(i <- r | P i) unwrap (S_ i)))
-             (\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
+  mxsum_spec (vs2mx (\sum_(i <- r | P i) unwrap (S_ i)))
+             (\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
Canonical nary_addv_expr := ProperSumvExpr nary_addv_subproof.
End Nary.

-Definition directv_def S of phantom {vspace vT} (unwrap (addv_val S)) :=
-  \dim (unwrap S) == unwrap (addv_dim S).
+Definition directv_def S of phantom {vspace vT} (unwrap (addv_val S)) :=
+  \dim (unwrap S) == unwrap (addv_dim S).

End SumExpr.
@@ -856,39 +855,39 @@
Lemma directvE (S : addv_expr) :
-  directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).
+  directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).

-Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).
+Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).

-Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).
+Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).

Lemma dimv_sum_leqif (S : addv_expr) :
-  \dim (unwrap S) ≤ unwrap (addv_dim S) ?= iff directv (unwrap S).
+  \dim (unwrap S) ≤ unwrap (addv_dim S) ?= iff directv (unwrap S).

Lemma directvEgeq (S : addv_expr) :
-  directv (unwrap S) = (\dim (unwrap S) ≥ unwrap (addv_dim S)).
+  directv (unwrap S) = (\dim (unwrap S) ≥ unwrap (addv_dim S)).

Section BinaryDirect.

Lemma directv_addE (S1 S2 : addv_expr) :
-  directv (unwrap S1 + unwrap S2)
-    = [&& directv (unwrap S1), directv (unwrap S2)
-        & unwrap S1 :&: unwrap S2 == 0]%VS.
+  directv (unwrap S1 + unwrap S2)
+    = [&& directv (unwrap S1), directv (unwrap S2)
+        & unwrap S1 :&: unwrap S2 == 0]%VS.

-Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
+Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).

Lemma directv_add_unique {U V} :
-   reflect (∀ u1 u2 v1 v2, u1 \in U → u2 \in U → v1 \in V → v2 \in V →
-             (u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2)))
-           (directv (U + V)).
+   reflect (∀ u1 u2 v1 v2, u1 \in U → u2 \in U → v1 \in V → v2 \in V →
+             (u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2)))
+           (directv (U + V)).

End BinaryDirect.
@@ -897,34 +896,34 @@ Section NaryDirect.

-Context {I : finType} {P : pred I}.
+Context {I : finType} {P : pred I}.

-Lemma directv_sumP {Us : I → {vspace vT}} :
-  reflect (∀ i, P i → Us i :&: (\sum_(j | P j && (j != i)) Us j) = 0)%VS
-          (directv (\sum_(i | P i) Us i)).
+Lemma directv_sumP {Us : I → {vspace vT}} :
+  reflect (∀ i, P i → Us i :&: (\sum_(j | P j && (j != i)) Us j) = 0)%VS
+          (directv (\sum_(i | P i) Us i)).

-Lemma directv_sumE {Ss : I → addv_expr} (xunwrap := unwrap) :
-  reflect [/\ ∀ i, P i → directv (unwrap (Ss i))
-            & directv (\sum_(i | P i) xunwrap (Ss i))]
-          (directv (\sum_(i | P i) unwrap (Ss i))).
+Lemma directv_sumE {Ss : I → addv_expr} (xunwrap := unwrap) :
+  reflect [/\ ∀ i, P i → directv (unwrap (Ss i))
+            & directv (\sum_(i | P i) xunwrap (Ss i))]
+          (directv (\sum_(i | P i) unwrap (Ss i))).

-Lemma directv_sum_independent {Us : I → {vspace vT}} :
-   reflect (∀ us,
-               (∀ i, P i → us i \in Us i) → \sum_(i | P i) us i = 0 →
-             (∀ i, P i → us i = 0))
-           (directv (\sum_(i | P i) Us i)).
+Lemma directv_sum_independent {Us : I → {vspace vT}} :
+   reflect (∀ us,
+               (∀ i, P i → us i \in Us i) → \sum_(i | P i) us i = 0 →
+             (∀ i, P i → us i = 0))
+           (directv (\sum_(i | P i) Us i)).

-Lemma directv_sum_unique {Us : I → {vspace vT}} :
-  reflect (∀ us vs,
-              (∀ i, P i → us i \in Us i) →
-              (∀ i, P i → vs i \in Us i) →
-            (\sum_(i | P i) us i == \sum_(i | P i) vs i)
-              = [∀ (i | P i), us i == vs i])
-          (directv (\sum_(i | P i) Us i)).
+Lemma directv_sum_unique {Us : I → {vspace vT}} :
+  reflect (∀ us vs,
+              (∀ i, P i → us i \in Us i) →
+              (∀ i, P i → vs i \in Us i) →
+            (\sum_(i | P i) us i == \sum_(i | P i) vs i)
+              = [∀ (i | P i), us i == vs i])
+          (directv (\sum_(i | P i) Us i)).

End NaryDirect.
@@ -936,37 +935,37 @@ Linear span generated by a list of vectors
-Lemma memv_span X v : v \in X → v \in <<X>>%VS.
+Lemma memv_span X v : v \in X → v \in <<X>>%VS.

-Lemma memv_span1 v : v \in <<[:: v]>>%VS.
+Lemma memv_span1 v : v \in <<[:: v]>>%VS.

-Lemma dim_span X : \dim <<X>> ≤ size X.
+Lemma dim_span X : \dim <<X>> ≤ size X.

-Lemma span_subvP {X U} : reflect {subset X ≤ U} (<<X>> ≤ U)%VS.
+Lemma span_subvP {X U} : reflect {subset X ≤ U} (<<X>> ≤ U)%VS.

-Lemma sub_span X Y : {subset X ≤ Y} → (<<X>> ≤ <<Y>>)%VS.
+Lemma sub_span X Y : {subset X ≤ Y} → (<<X>> ≤ <<Y>>)%VS.

-Lemma eq_span X Y : X =i Y → (<<X>> = <<Y>>)%VS.
+Lemma eq_span X Y : X =i Y → (<<X>> = <<Y>>)%VS.

-Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.
+Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.

-Lemma span_nil : (<<Nil vT>> = 0)%VS.
+Lemma span_nil : (<<Nil vT>> = 0)%VS.

-Lemma span_seq1 v : (<<[:: v]>> = <[v]>)%VS.
+Lemma span_seq1 v : (<<[:: v]>> = <[v]>)%VS.

-Lemma span_cons v X : (<<v :: X>> = <[v]> + <<X>>)%VS.
+Lemma span_cons v X : (<<v :: X>> = <[v]> + <<X>>)%VS.

-Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.
+Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.

@@ -977,22 +976,22 @@

-Definition coord_expanded_def n (X : n.-tuple vT) i v :=
-  (v2r v ×m pinvmx (b2mx X)) 0 i.
-Definition coord := locked_with span_key coord_expanded_def.
-Canonical coord_unlockable := [unlockable fun coord].
+Definition coord_expanded_def n (X : n.-tuple vT) i v :=
+  (v2r v ×m pinvmx (b2mx X)) 0 i.
+Definition coord := locked_with span_key coord_expanded_def.
+Canonical coord_unlockable := [unlockable fun coord].

-Fact coord_is_scalar n (X : n.-tuple vT) i : scalar (coord X i).
+Fact coord_is_scalar n (X : n.-tuple vT) i : scalar (coord X i).
Canonical coord_addidive n Xn i := Additive (@coord_is_scalar n Xn i).
Canonical coord_linear n Xn i := AddLinear (@coord_is_scalar n Xn i).

-Lemma coord_span n (X : n.-tuple vT) v :
-  v \in span X → v = \sum_i coord X i v *: X`_i.
+Lemma coord_span n (X : n.-tuple vT) v :
+  v \in span X → v = \sum_i coord X i v *: X`_i.

-Lemma coord0 i v : coord [tuple 0] i v = 0.
+Lemma coord0 i v : coord [tuple 0] i v = 0.

@@ -1006,65 +1005,65 @@ Lemma nil_free : free (Nil vT).

-Lemma seq1_free v : free [:: v] = (v != 0).
+Lemma seq1_free v : free [:: v] = (v != 0).

-Lemma perm_free X Y : perm_eq X Y → free X = free Y.
+Lemma perm_free X Y : perm_eq X Y → free X = free Y.

-Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).
+Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).

-Lemma free_not0 v X : free X → v \in X → v != 0.
+Lemma free_not0 v X : free X → v \in X → v != 0.

-Lemma freeP n (X : n.-tuple vT) :
-  reflect (∀ k, \sum_(i < n) k i *: X`_i = 0 → (∀ i, k i = 0))
+Lemma freeP n (X : n.-tuple vT) :
+  reflect (∀ k, \sum_(i < n) k i *: X`_i = 0 → (∀ i, k i = 0))
          (free X).

-Lemma coord_free n (X : n.-tuple vT) (i j : 'I_n) :
-  free X → coord X j (X`_i) = (i == j)%:R.
+Lemma coord_free n (X : n.-tuple vT) (i j : 'I_n) :
+  free X → coord X j (X`_i) = (i == j)%:R.

-Lemma coord_sum_free n (X : n.-tuple vT) k j :
-  free X → coord X j (\sum_(i < n) k i *: X`_i) = k j.
+Lemma coord_sum_free n (X : n.-tuple vT) k j :
+  free X → coord X j (\sum_(i < n) k i *: X`_i) = k j.

Lemma cat_free X Y :
-  free (X ++ Y) = [&& free X, free Y & directv (<<X>> + <<Y>>)].
+  free (X ++ Y) = [&& free X, free Y & directv (<<X>> + <<Y>>)].

-Lemma catl_free Y X : free (X ++ Y) → free X.
+Lemma catl_free Y X : free (X ++ Y) → free X.

-Lemma catr_free X Y : free (X ++ Y) → free Y.
+Lemma catr_free X Y : free (X ++ Y) → free Y.

-Lemma filter_free p X : free X → free (filter p X).
+Lemma filter_free p X : free X → free (filter p X).

-Lemma free_cons v X : free (v :: X) = (v \notin <<X>>)%VS && free X.
+Lemma free_cons v X : free (v :: X) = (v \notin <<X>>)%VS && free X.

-Lemma freeE n (X : n.-tuple vT) :
-  free X = [∀ i : 'I_n, X`_i \notin <<drop i.+1 X>>%VS].
+Lemma freeE n (X : n.-tuple vT) :
+  free X = [∀ i : 'I_n, X`_i \notin <<drop i.+1 X>>%VS].

-Lemma freeNE n (X : n.-tuple vT) :
-  ~~ free X = [∃ i : 'I_n, X`_i \in <<drop i.+1 X>>%VS].
+Lemma freeNE n (X : n.-tuple vT) :
+  ~~ free X = [∃ i : 'I_n, X`_i \in <<drop i.+1 X>>%VS].

-Lemma free_uniq X : free X → uniq X.
+Lemma free_uniq X : free X → uniq X.

-Lemma free_span X v (sumX := fun k ⇒ \sum_(x <- X) k x *: x) :
-    free X → v \in <<X>>%VS →
-  {k | v = sumX k & ∀ k1, v = sumX k1 → {in X, k1 =1 k}}.
+Lemma free_span X v (sumX := fun k ⇒ \sum_(x <- X) k x *: x) :
+    free X → v \in <<X>>%VS →
+  {k | v = sumX k & ∀ k1, v = sumX k1 → {in X, k1 =1 k}}.

Lemma linear_of_free (rT : lmodType K) X (fX : seq rT) :
-  {f : {linear vT → rT} | free X → size fX = size X → map f X = fX}.
+  {f : {linear vT → rT} | free X → size fX = size X → map f X = fX}.

@@ -1075,73 +1074,73 @@

-Lemma span_basis U X : basis_of U X → <<X>>%VS = U.
+Lemma span_basis U X : basis_of U X → <<X>>%VS = U.

-Lemma basis_free U X : basis_of U X → free X.
+Lemma basis_free U X : basis_of U X → free X.

-Lemma coord_basis U n (X : n.-tuple vT) v :
-  basis_of U X → v \in U → v = \sum_i coord X i v *: X`_i.
+Lemma coord_basis U n (X : n.-tuple vT) v :
+  basis_of U X → v \in U → v = \sum_i coord X i v *: X`_i.

Lemma nil_basis : basis_of 0 (Nil vT).

-Lemma seq1_basis v : v != 0 → basis_of <[v]> [:: v].
+Lemma seq1_basis v : v != 0 → basis_of <[v]> [:: v].

-Lemma basis_not0 x U X : basis_of U X → x \in X → x != 0.
+Lemma basis_not0 x U X : basis_of U X → x \in X → x != 0.

-Lemma basis_mem x U X : basis_of U X → x \in X → x \in U.
+Lemma basis_mem x U X : basis_of U X → x \in X → x \in U.

Lemma cat_basis U V X Y :
-  directv (U + V) → basis_of U X → basis_of V Y → basis_of (U + V) (X ++ Y).
+  directv (U + V) → basis_of U X → basis_of V Y → basis_of (U + V) (X ++ Y).

-Lemma size_basis U n (X : n.-tuple vT) : basis_of U X → \dim U = n.
+Lemma size_basis U n (X : n.-tuple vT) : basis_of U X → \dim U = n.

-Lemma basisEdim X U : basis_of U X = (U ≤ <<X>>)%VS && (size X ≤ \dim U).
+Lemma basisEdim X U : basis_of U X = (U ≤ <<X>>)%VS && (size X ≤ \dim U).

Lemma basisEfree X U :
-  basis_of U X = [&& free X, (<<X>> ≤ U)%VS & \dim U ≤ size X].
+  basis_of U X = [&& free X, (<<X>> ≤ U)%VS & \dim U ≤ size X].

-Lemma perm_basis X Y U : perm_eq X Y → basis_of U X = basis_of U Y.
+Lemma perm_basis X Y U : perm_eq X Y → basis_of U X = basis_of U Y.

Lemma vbasisP U : basis_of U (vbasis U).

-Lemma vbasis_mem v U : v \in (vbasis U) → v \in U.
+Lemma vbasis_mem v U : v \in (vbasis U) → v \in U.

Lemma coord_vbasis v U :
-  v \in U → v = \sum_(i < \dim U) coord (vbasis U) i v *: (vbasis U)`_i.
+  v \in U → v = \sum_(i < \dim U) coord (vbasis U) i v *: (vbasis U)`_i.

Section BigSumBasis.

-Variables (I : finType) (P : pred I) (Xs : I → seq vT).
+Variables (I : finType) (P : pred I) (Xs : I → seq vT).

Lemma span_bigcat :
-  (<<\big[cat/[::]]_(i | P i) Xs i>> = \sum_(i | P i) <<Xs i>>)%VS.
+  (<<\big[cat/[::]]_(i | P i) Xs i>> = \sum_(i | P i) <<Xs i>>)%VS.

Lemma bigcat_free :
-    directv (\sum_(i | P i) <<Xs i>>) →
-  (∀ i, P i → free (Xs i)) → free (\big[cat/[::]]_(i | P i) Xs i).
+    directv (\sum_(i | P i) <<Xs i>>) →
+  (∀ i, P i → free (Xs i)) → free (\big[cat/[::]]_(i | P i) Xs i).

-Lemma bigcat_basis Us (U := (\sum_(i | P i) Us i)%VS) :
-    directv U → (∀ i, P i → basis_of (Us i) (Xs i)) →
-  basis_of U (\big[cat/[::]]_(i | P i) Xs i).
+Lemma bigcat_basis Us (U := (\sum_(i | P i) Us i)%VS) :
+    directv U → (∀ i, P i → basis_of (Us i) (Xs i)) →
+  basis_of U (\big[cat/[::]]_(i | P i) Xs i).

End BigSumBasis.
@@ -1150,10 +1149,10 @@ End VectorTheory.

-Hint Resolve subvv.
+Hint Resolve subvv : core.

-Notation directv S := (directv_def (Phantom _ S%VS)).
+Notation directv S := (directv_def (Phantom _ S%VS)).

@@ -1169,28 +1168,28 @@ Implicit Types aT vT rT : vectType R.

-Fact lfun_key : unit.
-Definition fun_of_lfun_def aT rT (f : 'Hom(aT, rT)) :=
-  r2v \o mulmxr (f2mx f) \o v2r.
-Definition fun_of_lfun := locked_with lfun_key fun_of_lfun_def.
-Canonical fun_of_lfun_unlockable := [unlockable fun fun_of_lfun].
-Definition linfun_def aT rT (f : aT → rT) :=
-  Vector.Hom (lin1_mx (v2r \o f \o r2v)).
-Definition linfun := locked_with lfun_key linfun_def.
-Canonical linfun_unlockable := [unlockable fun linfun].
+Fact lfun_key : unit.
+Definition fun_of_lfun_def aT rT (f : 'Hom(aT, rT)) :=
+  r2v \o mulmxr (f2mx f) \o v2r.
+Definition fun_of_lfun := locked_with lfun_key fun_of_lfun_def.
+Canonical fun_of_lfun_unlockable := [unlockable fun fun_of_lfun].
+Definition linfun_def aT rT (f : aT → rT) :=
+  Vector.Hom (lin1_mx (v2r \o f \o r2v)).
+Definition linfun := locked_with lfun_key linfun_def.
+Canonical linfun_unlockable := [unlockable fun linfun].

-Definition id_lfun vT := @linfun vT vT idfun.
-Definition comp_lfun aT vT rT (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) :=
-  linfun (fun_of_lfun f \o fun_of_lfun g).
+Definition id_lfun vT := @linfun vT vT idfun.
+Definition comp_lfun aT vT rT (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) :=
+  linfun (fun_of_lfun f \o fun_of_lfun g).

End LfunDefs.

Coercion fun_of_lfun : Vector.hom >-> Funclass.
-Notation "\1" := (@id_lfun _ _) : lfun_scope.
-Notation "f \o g" := (comp_lfun f g) : lfun_scope.
+Notation "\1" := (@id_lfun _ _) : lfun_scope.
+Notation "f \o g" := (comp_lfun f g) : lfun_scope.

Section LfunVspaceDefs.
@@ -1200,23 +1199,23 @@ Implicit Types aT rT : vectType K.

-Definition inv_lfun aT rT (f : 'Hom(aT, rT)) := Vector.Hom (pinvmx (f2mx f)).
-Definition lker aT rT (f : 'Hom(aT, rT)) := mx2vs (kermx (f2mx f)).
-Fact lfun_img_key : unit.
-Definition lfun_img_def aT rT f (U : {vspace aT}) : {vspace rT} :=
-  mx2vs (vs2mx U ×m f2mx f).
-Definition lfun_img := locked_with lfun_img_key lfun_img_def.
-Canonical lfun_img_unlockable := [unlockable fun lfun_img].
-Definition lfun_preim aT rT (f : 'Hom(aT, rT)) W :=
-  (lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.
+Definition inv_lfun aT rT (f : 'Hom(aT, rT)) := Vector.Hom (pinvmx (f2mx f)).
+Definition lker aT rT (f : 'Hom(aT, rT)) := mx2vs (kermx (f2mx f)).
+Fact lfun_img_key : unit.
+Definition lfun_img_def aT rT f (U : {vspace aT}) : {vspace rT} :=
+  mx2vs (vs2mx U ×m f2mx f).
+Definition lfun_img := locked_with lfun_img_key lfun_img_def.
+Canonical lfun_img_unlockable := [unlockable fun lfun_img].
+Definition lfun_preim aT rT (f : 'Hom(aT, rT)) W :=
+  (lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.

End LfunVspaceDefs.

-Notation "f ^-1" := (inv_lfun f) : lfun_scope.
-Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
-Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
+Notation "f ^-1" := (inv_lfun f) : lfun_scope.
+Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
+Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
Notation limg f := (lfun_img f fullv).

@@ -1224,13 +1223,13 @@
Variables (R : ringType) (aT rT : vectType R).
-Implicit Types f g h : 'Hom(aT, rT).
+Implicit Types f g h : 'Hom(aT, rT).

-Canonical lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
-Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
-Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
-Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.
+Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
+Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
+Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
+Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.

Fact lfun_is_linear f : linear f.
@@ -1238,74 +1237,76 @@ Canonical lfun_linear f := AddLinear (lfun_is_linear f).

-Lemma lfunE (ff : {linear aT → rT}) : linfun ff =1 ff.
+Lemma lfunE (ff : {linear aT → rT}) : linfun ff =1 ff.

-Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.
+Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.

-Lemma lfunP f g : f =1 g ↔ f = g.
+Lemma lfunP f g : f =1 g ↔ f = g.

-Definition zero_lfun : 'Hom(aT, rT) := linfun \0.
-Definition add_lfun f g := linfun (f \+ g).
-Definition opp_lfun f := linfun (-%R \o f).
+Definition zero_lfun : 'Hom(aT, rT) := linfun \0.
+Definition add_lfun f g := linfun (f \+ g).
+Definition opp_lfun f := linfun (-%R \o f).

-Fact lfun_addA : associative add_lfun.
+Fact lfun_addA : associative add_lfun.

-Fact lfun_addC : commutative add_lfun.
+Fact lfun_addC : commutative add_lfun.

-Fact lfun_add0 : left_id zero_lfun add_lfun.
+Fact lfun_add0 : left_id zero_lfun add_lfun.

-Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.
+Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.

Definition lfun_zmodMixin := ZmodMixin lfun_addA lfun_addC lfun_add0 lfun_addN.
-Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom(aT, rT) lfun_zmodMixin.
+Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom(aT, rT) lfun_zmodMixin.

-Lemma zero_lfunE x : (0 : 'Hom(aT, rT)) x = 0.
-Lemma add_lfunE f g x : (f + g) x = f x + g x.
-Lemma opp_lfunE f x : (- f) x = - f x.
-Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I → 'Hom(aT, rT)) x :
-  (\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.
+Lemma zero_lfunE x : (0 : 'Hom(aT, rT)) x = 0.
+Lemma add_lfunE f g x : (f + g) x = f x + g x.
+Lemma opp_lfunE f x : (- f) x = - f x.
+Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I → 'Hom(aT, rT)) x :
+  (\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.

End LfunZmodType.
+
+
Section LfunVectType.

Variables (R : comRingType) (aT rT : vectType R).
-Implicit Types f : 'Hom(aT, rT).
+Implicit Types f : 'Hom(aT, rT).

-Definition scale_lfun k f := linfun (k \*: f).
+Definition scale_lfun k f := linfun (k \*: f).

-Fact lfun_scaleA k1 k2 f : k1 *:l (k2 *:l f) = (k1 × k2) *:l f.
+Fact lfun_scaleA k1 k2 f : k1 *:l (k2 *:l f) = (k1 × k2) *:l f.

-Fact lfun_scale1 f : 1 *:l f = f.
+Fact lfun_scale1 f : 1 *:l f = f.

-Fact lfun_scaleDr k f1 f2 : k *:l (f1 + f2) = k *:l f1 + k *:l f2.
+Fact lfun_scaleDr k f1 f2 : k *:l (f1 + f2) = k *:l f1 + k *:l f2.

-Fact lfun_scaleDl f k1 k2 : (k1 + k2) *:l f = k1 *:l f + k2 *:l f.
+Fact lfun_scaleDl f k1 k2 : (k1 + k2) *:l f = k1 *:l f + k2 *:l f.

Definition lfun_lmodMixin :=
  LmodMixin lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.
-Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom(aT, rT) lfun_lmodMixin.
+Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom(aT, rT) lfun_lmodMixin.

-Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
+Lemma scale_lfunE k f x : (k *: f) x = k *: f x.

@@ -1315,11 +1316,11 @@ probably because of incomplete type unification. Will it work in 8.4?
-Fact lfun_vect_iso : Vector.axiom (Vector.dim aT × Vector.dim rT) 'Hom(aT, rT).
+Fact lfun_vect_iso : Vector.axiom (Vector.dim aT × Vector.dim rT) 'Hom(aT, rT).

Definition lfun_vectMixin := VectMixin lfun_vect_iso.
-Canonical lfun_vectType := VectType R 'Hom(aT, rT) lfun_vectMixin.
+Canonical lfun_vectType := VectType R 'Hom(aT, rT) lfun_vectMixin.

End LfunVectType.
@@ -1329,58 +1330,58 @@
Variables (R : ringType) (wT aT vT rT : vectType R).
-Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) (h : 'Hom(wT, aT)).
+Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) (h : 'Hom(wT, aT)).

-Lemma id_lfunE u: \1%VF u = u :> aT.
-Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u).
+Lemma id_lfunE u: \1%VF u = u :> aT.
+Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u).

-Lemma comp_lfunA f g h : (f \o (g \o h) = (f \o g) \o h)%VF.
+Lemma comp_lfunA f g h : (f \o (g \o h) = (f \o g) \o h)%VF.

-Lemma comp_lfun1l f : (\1 \o f)%VF = f.
+Lemma comp_lfun1l f : (\1 \o f)%VF = f.

-Lemma comp_lfun1r f : (f \o \1)%VF = f.
+Lemma comp_lfun1r f : (f \o \1)%VF = f.

-Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom(aT, rT).
+Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom(aT, rT).

-Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).
+Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).

-Lemma comp_lfunDl f1 f2 g : ((f1 + f2) \o g = (f1 \o g) + (f2 \o g))%VF.
+Lemma comp_lfunDl f1 f2 g : ((f1 + f2) \o g = (f1 \o g) + (f2 \o g))%VF.

-Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2) = (f \o g1) + (f \o g2))%VF.
+Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2) = (f \o g1) + (f \o g2))%VF.

-Lemma comp_lfunNl f g : ((- f) \o g = - (f \o g))%VF.
+Lemma comp_lfunNl f g : ((- f) \o g = - (f \o g))%VF.

-Lemma comp_lfunNr f g : (f \o (- g) = - (f \o g))%VF.
+Lemma comp_lfunNr f g : (f \o (- g) = - (f \o g))%VF.

End CompLfun.

Definition lfun_simp :=
-  (comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).
+  (comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).

Section ScaleCompLfun.

Variables (R : comRingType) (aT vT rT : vectType R).
-Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)).
+Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)).

-Lemma comp_lfunZl k f g : (k *: (f \o g) = (k *: f) \o g)%VF.
+Lemma comp_lfunZl k f g : (k *: (f \o g) = (k *: f) \o g)%VF.

-Lemma comp_lfunZr k f g : (k *: (f \o g) = f \o (k *: g))%VF.
+Lemma comp_lfunZr k f g : (k *: (f \o g) = f \o (k *: g))%VF.

End ScaleCompLfun.
@@ -1390,95 +1391,95 @@
Variables (K : fieldType) (aT rT : vectType K).
-Implicit Types (f g : 'Hom(aT, rT)) (U V : {vspace aT}) (W : {vspace rT}).
+Implicit Types (f g : 'Hom(aT, rT)) (U V : {vspace aT}) (W : {vspace rT}).

-Lemma limgS f U V : (U ≤ V)%VS → (f @: U ≤ f @: V)%VS.
+Lemma limgS f U V : (U ≤ V)%VS → (f @: U ≤ f @: V)%VS.

-Lemma limg_line f v : (f @: <[v]> = <[f v]>)%VS.
+Lemma limg_line f v : (f @: <[v]> = <[f v]>)%VS.

-Lemma limg0 f : (f @: 0 = 0)%VS.
+Lemma limg0 f : (f @: 0 = 0)%VS.

-Lemma memv_img f v U : v \in U → f v \in (f @: U)%VS.
+Lemma memv_img f v U : v \in U → f v \in (f @: U)%VS.

Lemma memv_imgP f w U :
-  reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
+  reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.

-Lemma lim0g U : (0 @: U = 0 :> {vspace rT})%VS.
+Lemma lim0g U : (0 @: U = 0 :> {vspace rT})%VS.

-Lemma eq_in_limg V f g : {in V, f =1 g} → (f @: V = g @: V)%VS.
+Lemma eq_in_limg V f g : {in V, f =1 g} → (f @: V = g @: V)%VS.

-Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.
+Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.

-Lemma limg_sum f I r (P : pred I) Us :
-  (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS.
+Lemma limg_sum f I r (P : pred I) Us :
+  (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS.

-Lemma limg_cap f U V : (f @: (U :&: V) ≤ f @: U :&: f @: V)%VS.
+Lemma limg_cap f U V : (f @: (U :&: V) ≤ f @: U :&: f @: V)%VS.

-Lemma limg_bigcap f I r (P : pred I) Us :
-  (f @: (\bigcap_(i <- r | P i) Us i) ≤ \bigcap_(i <- r | P i) f @: Us i)%VS.
+Lemma limg_bigcap f I r (P : pred I) Us :
+  (f @: (\bigcap_(i <- r | P i) Us i) ≤ \bigcap_(i <- r | P i) f @: Us i)%VS.

-Lemma limg_span f X : (f @: <<X>> = <<map f X>>)%VS.
+Lemma limg_span f X : (f @: <<X>> = <<map f X>>)%VS.

-Lemma lfunPn f g : reflect (∃ u, f u != g u) (f != g).
+Lemma lfunPn f g : reflect (∃ u, f u != g u) (f != g).

-Lemma inv_lfun_def f : (f \o f^-1 \o f)%VF = f.
+Lemma inv_lfun_def f : (f \o f^-1 \o f)%VF = f.

-Lemma limg_lfunVK f : {in limg f, cancel f^-1%VF f}.
+Lemma limg_lfunVK f : {in limg f, cancel f^-1%VF f}.

-Lemma lkerE f U : (U ≤ lker f)%VS = (f @: U == 0)%VS.
+Lemma lkerE f U : (U ≤ lker f)%VS = (f @: U == 0)%VS.

-Lemma memv_ker f v : (v \in lker f) = (f v == 0).
+Lemma memv_ker f v : (v \in lker f) = (f v == 0).

-Lemma eqlfunP f g v : reflect (f v = g v) (v \in lker (f - g)).
+Lemma eqlfunP f g v : reflect (f v = g v) (v \in lker (f - g)).

-Lemma eqlfun_inP V f g : reflect {in V, f =1 g} (V ≤ lker (f - g))%VS.
+Lemma eqlfun_inP V f g : reflect {in V, f =1 g} (V ≤ lker (f - g))%VS.

-Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.
+Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.

-Lemma limg_ker_dim f U : (\dim (U :&: lker f) + \dim (f @: U) = \dim U)%N.
+Lemma limg_ker_dim f U : (\dim (U :&: lker f) + \dim (f @: U) = \dim U)%N.

-Lemma limg_dim_eq f U : (U :&: lker f = 0)%VS → \dim (f @: U) = \dim U.
+Lemma limg_dim_eq f U : (U :&: lker f = 0)%VS → \dim (f @: U) = \dim U.

Lemma limg_basis_of f U X :
-  (U :&: lker f = 0)%VS → basis_of U X → basis_of (f @: U) (map f X).
+  (U :&: lker f = 0)%VS → basis_of U X → basis_of (f @: U) (map f X).

-Lemma lker0P f : reflect (injective f) (lker f == 0%VS).
+Lemma lker0P f : reflect (injective f) (lker f == 0%VS).

-Lemma limg_ker0 f U V : lker f == 0%VS → (f @: U ≤ f @: V)%VS = (U ≤ V)%VS.
+Lemma limg_ker0 f U V : lker f == 0%VS → (f @: U ≤ f @: V)%VS = (U ≤ V)%VS.

-Lemma eq_limg_ker0 f U V : lker f == 0%VS → (f @: U == f @: V)%VS = (U == V).
+Lemma eq_limg_ker0 f U V : lker f == 0%VS → (f @: U == f @: V)%VS = (U == V).

-Lemma lker0_lfunK f : lker f == 0%VS → cancel f f^-1%VF.
+Lemma lker0_lfunK f : lker f == 0%VS → cancel f f^-1%VF.

-Lemma lker0_compVf f : lker f == 0%VS → (f^-1 \o f = \1)%VF.
+Lemma lker0_compVf f : lker f == 0%VS → (f^-1 \o f = \1)%VF.

End LinearImage.
@@ -1490,22 +1491,22 @@
Variables (K : fieldType) (vT : vectType K).
-Implicit Types (f : 'End(vT)) (U : {vspace vT}).
+Implicit Types (f : 'End(vT)) (U : {vspace vT}).

-Definition fixedSpace f : {vspace vT} := lker (f - \1%VF).
+Definition fixedSpace f : {vspace vT} := lker (f - \1%VF).

-Lemma fixedSpaceP f a : reflect (f a = a) (a \in fixedSpace f).
+Lemma fixedSpaceP f a : reflect (f a = a) (a \in fixedSpace f).

-Lemma fixedSpacesP f U : reflect {in U, f =1 id} (U ≤ fixedSpace f)%VS.
+Lemma fixedSpacesP f U : reflect {in U, f =1 id} (U ≤ fixedSpace f)%VS.

-Lemma fixedSpace_limg f U : (U ≤ fixedSpace f → f @: U = U)%VS.
+Lemma fixedSpace_limg f U : (U ≤ fixedSpace f → f @: U = U)%VS.

-Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS.
+Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS.

End FixedSpace.
@@ -1516,29 +1517,29 @@ Section LinAut.

-Variables (K : fieldType) (vT : vectType K) (f : 'End(vT)).
-Hypothesis kerf0 : lker f == 0%VS.
+Variables (K : fieldType) (vT : vectType K) (f : 'End(vT)).
+Hypothesis kerf0 : lker f == 0%VS.

-Lemma lker0_limgf : limg f = fullv.
+Lemma lker0_limgf : limg f = fullv.

-Lemma lker0_lfunVK : cancel f^-1%VF f.
+Lemma lker0_lfunVK : cancel f^-1%VF f.

-Lemma lker0_compfV : (f \o f^-1 = \1)%VF.
+Lemma lker0_compfV : (f \o f^-1 = \1)%VF.

-Lemma lker0_compVKf aT g : (f \o (f^-1 \o g))%VF = g :> 'Hom(aT, vT).
+Lemma lker0_compVKf aT g : (f \o (f^-1 \o g))%VF = g :> 'Hom(aT, vT).

-Lemma lker0_compKf aT g : (f^-1 \o (f \o g))%VF = g :> 'Hom(aT, vT).
+Lemma lker0_compKf aT g : (f^-1 \o (f \o g))%VF = g :> 'Hom(aT, vT).

-Lemma lker0_compfK rT h : ((h \o f) \o f^-1)%VF = h :> 'Hom(vT, rT).
+Lemma lker0_compfK rT h : ((h \o f) \o f^-1)%VF = h :> 'Hom(vT, rT).

-Lemma lker0_compfVK rT h : ((h \o f^-1) \o f)%VF = h :> 'Hom(vT, rT).
+Lemma lker0_compfVK rT h : ((h \o f^-1) \o f)%VF = h :> 'Hom(vT, rT).

End LinAut.
@@ -1548,13 +1549,13 @@
Variables (K : fieldType) (aT vT rT : vectType K).
-Implicit Types (f : 'Hom(aT, vT)) (g : 'Hom(vT, rT)) (U : {vspace aT}).
+Implicit Types (f : 'Hom(aT, vT)) (g : 'Hom(vT, rT)) (U : {vspace aT}).

-Lemma lim1g U : (\1 @: U)%VS = U.
+Lemma lim1g U : (\1 @: U)%VS = U.

-Lemma limg_comp f g U : ((g \o f) @: U = g @: (f @: U))%VS.
+Lemma limg_comp f g U : ((g \o f) @: U = g @: (f @: U))%VS.

End LinearImageComp.
@@ -1564,26 +1565,28 @@
Variables (K : fieldType) (aT rT : vectType K).
-Implicit Types (f : 'Hom(aT, rT)) (U : {vspace aT}) (V W : {vspace rT}).
+Implicit Types (f : 'Hom(aT, rT)) (U : {vspace aT}) (V W : {vspace rT}).

-Lemma lpreim_cap_limg f W : (f @^-1: (W :&: limg f))%VS = (f @^-1: W)%VS.
+Lemma lpreim_cap_limg f W : (f @^-1: (W :&: limg f))%VS = (f @^-1: W)%VS.

-Lemma lpreim0 f : (f @^-1: 0)%VS = lker f.
+Lemma lpreim0 f : (f @^-1: 0)%VS = lker f.

-Lemma lpreimS f V W : (V ≤ W)%VS→ (f @^-1: V ≤ f @^-1: W)%VS.
+Lemma lpreimS f V W : (V ≤ W)%VS→ (f @^-1: V ≤ f @^-1: W)%VS.

-Lemma lpreimK f W : (W ≤ limg f)%VS → (f @: (f @^-1: W))%VS = W.
+Lemma lpreimK f W : (W ≤ limg f)%VS → (f @: (f @^-1: W))%VS = W.

-Lemma memv_preim f u W : (f u \in W) = (u \in f @^-1: W)%VS.
+Lemma memv_preim f u W : (f u \in W) = (u \in f @^-1: W)%VS.

End LinearPreimage.
+
+
Section LfunAlgebra.
@@ -1600,10 +1603,10 @@
Variables (R : comRingType) (vT : vectType R).
-Hypothesis vT_proper : Vector.dim vT > 0.
+Hypothesis vT_proper : Vector.dim vT > 0.

-Fact lfun1_neq0 : \1%VF != 0 :> 'End(vT).
+Fact lfun1_neq0 : \1%VF != 0 :> 'End(vT).

@@ -1611,7 +1614,7 @@ Definition lfun_comp_ringMixin :=
  RingMixin comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr
            lfun1_neq0.
-Definition lfun_comp_ringType := RingType 'End(vT) lfun_comp_ringMixin.
+Definition lfun_comp_ringType := RingType 'End(vT) lfun_comp_ringMixin.

@@ -1622,11 +1625,11 @@
Definition lfun_ringMixin : GRing.Ring.mixin_of (lfun_zmodType vT vT) :=
  GRing.converse_ringMixin lfun_comp_ringType.
-Definition lfun_ringType := Eval hnf in RingType 'End(vT) lfun_ringMixin.
-Definition lfun_lalgType := Eval hnf in [lalgType R of 'End(vT)
-  for LalgType R lfun_ringType (fun k x y ⇒ comp_lfunZr k y x)].
-Definition lfun_algType := Eval hnf in [algType R of 'End(vT)
-  for AlgType R _ (fun k (x y : lfun_lalgType) ⇒ comp_lfunZl k y x)].
+Definition lfun_ringType := Eval hnf in RingType 'End(vT) lfun_ringMixin.
+Definition lfun_lalgType := Eval hnf in [lalgType R of 'End(vT)
+  for LalgType R lfun_ringType (fun k x y ⇒ comp_lfunZr k y x)].
+Definition lfun_algType := Eval hnf in [algType R of 'End(vT)
+  for AlgType R _ (fun k (x y : lfun_lalgType) ⇒ comp_lfunZl k y x)].

End LfunAlgebra.
@@ -1636,92 +1639,92 @@
Variables (K : fieldType) (vT : vectType K).
-Implicit Types U V : {vspace vT}.
+Implicit Types U V : {vspace vT}.

Definition daddv_pi U V := Vector.Hom (proj_mx (vs2mx U) (vs2mx V)).
-Definition projv U := daddv_pi U U^C.
-Definition addv_pi1 U V := daddv_pi (U :\: V) V.
-Definition addv_pi2 U V := daddv_pi V (U :\: V).
+Definition projv U := daddv_pi U U^C.
+Definition addv_pi1 U V := daddv_pi (U :\: V) V.
+Definition addv_pi2 U V := daddv_pi V (U :\: V).

-Lemma memv_pi U V w : (daddv_pi U V) w \in U.
+Lemma memv_pi U V w : (daddv_pi U V) w \in U.

-Lemma memv_proj U w : projv U w \in U.
+Lemma memv_proj U w : projv U w \in U.

-Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.
+Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.

-Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V.
+Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V.

-Lemma daddv_pi_id U V u : (U :&: V = 0)%VS → u \in U → daddv_pi U V u = u.
+Lemma daddv_pi_id U V u : (U :&: V = 0)%VS → u \in U → daddv_pi U V u = u.

Lemma daddv_pi_proj U V w (pi := daddv_pi U V) :
-  (U :&: V = 0)%VS → pi (pi w) = pi w.
+  (U :&: V = 0)%VS → pi (pi w) = pi w.

Lemma daddv_pi_add U V w :
-  (U :&: V = 0)%VS → (w \in U + V)%VS → daddv_pi U V w + daddv_pi V U w = w.
+  (U :&: V = 0)%VS → (w \in U + V)%VS → daddv_pi U V w + daddv_pi V U w = w.

-Lemma projv_id U u : u \in U → projv U u = u.
+Lemma projv_id U u : u \in U → projv U u = u.

-Lemma projv_proj U w : projv U (projv U w) = projv U w.
+Lemma projv_proj U w : projv U (projv U w) = projv U w.

-Lemma memv_projC U w : w - projv U w \in (U^C)%VS.
+Lemma memv_projC U w : w - projv U w \in (U^C)%VS.

-Lemma limg_proj U : limg (projv U) = U.
+Lemma limg_proj U : limg (projv U) = U.

-Lemma lker_proj U : lker (projv U) = (U^C)%VS.
+Lemma lker_proj U : lker (projv U) = (U^C)%VS.

-Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.
+Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.

-Lemma addv_pi2_id U V v : v \in V → addv_pi2 U V v = v.
+Lemma addv_pi2_id U V v : v \in V → addv_pi2 U V v = v.

-Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
+Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.

Lemma addv_pi1_pi2 U V w :
-  w \in (U + V)%VS → addv_pi1 U V w + addv_pi2 U V w = w.
+  w \in (U + V)%VS → addv_pi1 U V w + addv_pi2 U V w = w.

Section Sumv_Pi.

-Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I → {vspace vT}).
+Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I → {vspace vT}).

Let sumv_pi_rec i :=
-  fix loop r := if r is j :: r1 then
-    let V1 := (\sum_(k <- r1) Vs k)%VS in
-    if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
+  fix loop r := if r is j :: r1 then
+    let V1 := (\sum_(k <- r1) Vs k)%VS in
+    if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
  else 0.

-Notation sumV := (\sum_(i <- r0 | P i) Vs i)%VS.
-Definition sumv_pi_for V of V = sumV := fun i ⇒ sumv_pi_rec i (filter P r0).
+Notation sumV := (\sum_(i <- r0 | P i) Vs i)%VS.
+Definition sumv_pi_for V of V = sumV := fun i ⇒ sumv_pi_rec i (filter P r0).

-Variables (V : {vspace vT}) (defV : V = sumV).
+Variables (V : {vspace vT}) (defV : V = sumV).

-Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.
+Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.

Lemma sumv_pi_uniq_sum v :
-    uniq (filter P r0) → v \in V →
-  \sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
+    uniq (filter P r0) → v \in V →
+  \sum_(i <- r0 | P i) sumv_pi_for defV i v = v.

End Sumv_Pi.
@@ -1730,7 +1733,7 @@ End Projection.

-Notation sumv_pi V := (sumv_pi_for (erefl V)).
+Notation sumv_pi V := (sumv_pi_for (erefl V)).

Section SumvPi.
@@ -1739,14 +1742,14 @@ Variable (K : fieldType) (vT : vectType K).

-Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
-                  (defV : V = (\sum_(i | P i) Vs i)%VS) :
-  v \in V → \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
+Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
+                  (defV : V = (\sum_(i | P i) Vs i)%VS) :
+  v \in V → \sum_(i | P i) sumv_pi_for defV i v = v :> vT.

-Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
-                      (defV : V = (\sum_(m ≤ i < n | P i) Vs i)%VS) :
-  v \in V → \sum_(m ≤ i < n | P i) sumv_pi_for defV i v = v :> vT.
+Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
+                      (defV : V = (\sum_(m ≤ i < n | P i) Vs i)%VS) :
+  v \in V → \sum_(m ≤ i < n | P i) sumv_pi_for defV i v = v :> vT.

End SumvPi.
@@ -1761,27 +1764,27 @@ Turn a {vspace V} into a vectType
-Variable (K : fieldType) (vT : vectType K) (U : {vspace vT}).
+Variable (K : fieldType) (vT : vectType K) (U : {vspace vT}).

-Inductive subvs_of : predArgType := Subvs u & u \in U.
+Inductive subvs_of : predArgType := Subvs u & u \in U.

Definition vsval w := let: Subvs u _ := w in u.
-Canonical subvs_subType := Eval hnf in [subType for vsval].
-Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
+Canonical subvs_subType := Eval hnf in [subType for vsval].
+Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
Canonical subvs_eqType := Eval hnf in EqType subvs_of subvs_eqMixin.
-Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
+Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
Canonical subvs_choiceType := ChoiceType subvs_of subvs_choiceMixin.
-Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
+Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
Canonical subvs_zmodType := ZmodType subvs_of subvs_zmodMixin.
-Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
+Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
Canonical subvs_lmodType := LmodType K subvs_of subvs_lmodMixin.

-Lemma subvsP w : vsval w \in U.
-Lemma subvs_inj : injective vsval.
-Lemma congr_subvs u v : u = v → vsval u = vsval v.
+Lemma subvsP w : vsval w \in U.
+Lemma subvs_inj : injective vsval.
+Lemma congr_subvs u v : u = v → vsval u = vsval v.

Lemma vsval_is_linear : linear vsval.
@@ -1789,14 +1792,14 @@ Canonical vsval_linear := AddLinear vsval_is_linear.

-Fact vsproj_key : unit.
+Fact vsproj_key : unit.
Definition vsproj_def u := Subvs (memv_proj U u).
-Definition vsproj := locked_with vsproj_key vsproj_def.
-Canonical vsproj_unlockable := [unlockable fun vsproj].
+Definition vsproj := locked_with vsproj_key vsproj_def.
+Canonical vsproj_unlockable := [unlockable fun vsproj].

-Lemma vsprojK : {in U, cancel vsproj vsval}.
- Lemma vsvalK : cancel vsval vsproj.
+Lemma vsprojK : {in U, cancel vsproj vsval}.
+ Lemma vsvalK : cancel vsval vsproj.

Lemma vsproj_is_linear : linear vsproj.
@@ -1804,7 +1807,7 @@ Canonical vsproj_linear := AddLinear vsproj_is_linear.

-Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
+Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.

Definition subvs_vectMixin := VectMixin subvs_vect_iso.
@@ -1817,7 +1820,7 @@ Section MatrixVectType.

-Variables (R : ringType) (m n : nat).
+Variables (R : ringType) (m n : nat).

@@ -1827,9 +1830,9 @@ expansions that the Ltac interpretation of exists is incapable of doing.
-Fact matrix_vect_iso : Vector.axiom (m × n) 'M[R]_(m, n).
+Fact matrix_vect_iso : Vector.axiom (m × n) 'M[R]_(m, n).
Definition matrix_vectMixin := VectMixin matrix_vect_iso.
-Canonical matrix_vectType := VectType R 'M[R]_(m, n) matrix_vectMixin.
+Canonical matrix_vectType := VectType R 'M[R]_(m, n) matrix_vectMixin.

End MatrixVectType.
@@ -1847,9 +1850,9 @@ Variable R : ringType.

-Fact regular_vect_iso : Vector.axiom 1 R^o.
+Fact regular_vect_iso : Vector.axiom 1 R^o.
Definition regular_vectMixin := VectMixin regular_vect_iso.
-Canonical regular_vectType := VectType R R^o regular_vectMixin.
+Canonical regular_vectType := VectType R R^o regular_vectMixin.

End RegularVectType.
@@ -1867,9 +1870,9 @@ Variables (R : ringType) (vT1 vT2 : vectType R).

-Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 × vT2).
+Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 × vT2).
Definition pair_vectMixin := VectMixin pair_vect_iso.
-Canonical pair_vectType := VectType R (vT1 × vT2) pair_vectMixin.
+Canonical pair_vectType := VectType R (vT1 × vT2) pair_vectMixin.

End ProdVector.
@@ -1893,18 +1896,18 @@ Type unification with exist is again a problem in this proof.
-Fact ffun_vect_iso : Vector.axiom (#|I| × Vector.dim vT) {ffun I → vT}.
+Fact ffun_vect_iso : Vector.axiom (#|I| × Vector.dim vT) {ffun I → vT}.

Definition ffun_vectMixin := VectMixin ffun_vect_iso.
-Canonical ffun_vectType := VectType R {ffun I → vT} ffun_vectMixin.
+Canonical ffun_vectType := VectType R {ffun I → vT} ffun_vectMixin.

End FunVectType.

Canonical exp_vectType (K : fieldType) (vT : vectType K) n :=
-  [vectType K of vT ^ n].
+  [vectType K of vT ^ n].

@@ -1917,15 +1920,15 @@
Variable (K : fieldType) (vT : vectType K).
-Variables (n : nat) (lhs : n.-tuple 'End(vT)) (rhs : n.-tuple vT).
+Variables (n : nat) (lhs : n.-tuple 'End(vT)) (rhs : n.-tuple vT).

-Let lhsf u := finfun ((tnth lhs)^~ u).
-Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.
+Let lhsf u := finfun ((tnth lhs)^~ u).
+Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.

-Lemma vsolve_eqP (U : {vspace vT}) :
-  reflect (exists2 u, u \in U & ∀ i, tnth lhs i u = tnth rhs i)
+Lemma vsolve_eqP (U : {vspace vT}) :
+  reflect (exists2 u, u \in U & ∀ i, tnth lhs i u = tnth rhs i)
          (vsolve_eq U).

-- cgit v1.2.3