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.mxpoly.html | 390 ++++++++++++++++-------------- 1 file changed, 211 insertions(+), 179 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.mxpoly.html') diff --git a/docs/htmldoc/mathcomp.algebra.mxpoly.html b/docs/htmldoc/mathcomp.algebra.mxpoly.html index f9e95f9..81cbeb0 100644 --- a/docs/htmldoc/mathcomp.algebra.mxpoly.html +++ b/docs/htmldoc/mathcomp.algebra.mxpoly.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.

@@ -44,10 +43,11 @@ powers_mx A d == the d x (n ^ 2) matrix whose rows are the mxvec encodings of the first d powers of A (n of the form n'.+1). Thus, vec_mx (v *m powers_mx A d) = horner_mx A (rVpoly v). - char_poly A == the characteristic polynomial of A. - char_poly_mx A == a matrix whose detereminant is char_poly A. - mxminpoly A == the minimal polynomial of A, i.e., the smallest monic - polynomial that annihilates A (A must be nontrivial). + char_poly A == the characteristic polynomial of A. + char_poly_mx A == a matrix whose determinant is char_poly A. + companionmx p == a matrix whose char_poly is p + mxminpoly A == the minimal polynomial of A, i.e., the smallest monic + polynomial that annihilates A (A must be nontrivial). degree_mxminpoly A == the (positive) degree of mxminpoly A. mx_inv_horner A == the inverse of horner_mx A for polynomials of degree smaller than degree_mxminpoly A. @@ -97,28 +97,28 @@ Section RowPoly.

-Variables (R : ringType) (d : nat).
-Implicit Types u v : 'rV[R]_d.
-Implicit Types p q : {poly R}.
+Variables (R : ringType) (d : nat).
+Implicit Types u v : 'rV[R]_d.
+Implicit Types p q : {poly R}.

-Definition rVpoly v := \poly_(k < d) (if insub k is Some i then v 0 i else 0).
-Definition poly_rV p := \row_(i < d) p`_i.
+Definition rVpoly v := \poly_(k < d) (if insub k is Some i then v 0 i else 0).
+Definition poly_rV p := \row_(i < d) p`_i.

-Lemma coef_rVpoly v k : (rVpoly v)`_k = if insub k is Some i then v 0 i else 0.
+Lemma coef_rVpoly v k : (rVpoly v)`_k = if insub k is Some i then v 0 i else 0.

-Lemma coef_rVpoly_ord v (i : 'I_d) : (rVpoly v)`_i = v 0 i.
+Lemma coef_rVpoly_ord v (i : 'I_d) : (rVpoly v)`_i = v 0 i.

-Lemma rVpoly_delta i : rVpoly (delta_mx 0 i) = 'X^i.
+Lemma rVpoly_delta i : rVpoly (delta_mx 0 i) = 'X^i.

-Lemma rVpolyK : cancel rVpoly poly_rV.
+Lemma rVpolyK : cancel rVpoly poly_rV.

-Lemma poly_rV_K p : size p ≤ d → rVpoly (poly_rV p) = p.
+Lemma poly_rV_K p : size p ≤ d → rVpoly (poly_rV p) = p.

Lemma poly_rV_is_linear : linear poly_rV.
@@ -139,200 +139,224 @@ Section Resultant.

-Variables (R : ringType) (p q : {poly R}).
+Variables (R : ringType) (p q : {poly R}).

-Let dS := ((size q).-1 + (size p).-1)%N.
+Let dS := ((size q).-1 + (size p).-1)%N.

-Definition Sylvester_mx : 'M[R]_dS := col_mx (band p) (band q).
+Definition Sylvester_mx : 'M[R]_dS := col_mx (band p) (band q).

-Lemma Sylvester_mxE (i j : 'I_dS) :
-  let S_ r k := r`_(j - k) *+ (k ≤ j) in
-  Sylvester_mx i j = match split i with inl k ⇒ S_ p k | inr k ⇒ S_ q k end.
+Lemma Sylvester_mxE (i j : 'I_dS) :
+  let S_ r k := r`_(j - k) *+ (k ≤ j) in
+  Sylvester_mx i j = match split i with inl k ⇒ S_ p k | inr k ⇒ S_ q k end.

-Definition resultant := \det Sylvester_mx.
+Definition resultant := \det Sylvester_mx.

End Resultant.

-Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) :
-    size p > 1 → size q > 1 →
-  {uv : {poly R} × {poly R} | size uv.1 < size q ∧ size uv.2 < size p
-  & (resultant p q)%:P = uv.1 × p + uv.2 × q}.

-Lemma resultant_eq0 (R : idomainType) (p q : {poly R}) :
-  (resultant p q == 0) = (size (gcdp p q) > 1).
+Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) :
+    size p > 1 → size q > 1 →
+  {uv : {poly R} × {poly R} | size uv.1 < size q ∧ size uv.2 < size p
+  & (resultant p q)%:P = uv.1 × p + uv.2 × q}.
+ +
+Lemma resultant_eq0 (R : idomainType) (p q : {poly R}) :
+  (resultant p q == 0) = (size (gcdp p q) > 1).

Section HornerMx.

-Variables (R : comRingType) (n' : nat).
-Variable A : 'M[R]_n.
-Implicit Types p q : {poly R}.
+Variables (R : comRingType) (n' : nat).
+Variable A : 'M[R]_n.
+Implicit Types p q : {poly R}.

Definition horner_mx := horner_morph (fun a ⇒ scalar_mx_comm a A).
-Canonical horner_mx_additive := [additive of horner_mx].
-Canonical horner_mx_rmorphism := [rmorphism of horner_mx].
+Canonical horner_mx_additive := [additive of horner_mx].
+Canonical horner_mx_rmorphism := [rmorphism of horner_mx].

-Lemma horner_mx_C a : horner_mx a%:P = a%:M.
+Lemma horner_mx_C a : horner_mx a%:P = a%:M.

-Lemma horner_mx_X : horner_mx 'X = A.
+Lemma horner_mx_X : horner_mx 'X = A.

Lemma horner_mxZ : scalable horner_mx.

Canonical horner_mx_linear := AddLinear horner_mxZ.
-Canonical horner_mx_lrmorphism := [lrmorphism of horner_mx].
+Canonical horner_mx_lrmorphism := [lrmorphism of horner_mx].

-Definition powers_mx d := \matrix_(i < d) mxvec (A ^+ i).
+Definition powers_mx d := \matrix_(i < d) mxvec (A ^+ i).

-Lemma horner_rVpoly m (u : 'rV_m) :
-  horner_mx (rVpoly u) = vec_mx (u ×m powers_mx m).
+Lemma horner_rVpoly m (u : 'rV_m) :
+  horner_mx (rVpoly u) = vec_mx (u ×m powers_mx m).

End HornerMx.
+
+
Section CharPoly.

-Variables (R : ringType) (n : nat) (A : 'M[R]_n).
-Implicit Types p q : {poly R}.
+Variables (R : ringType) (n : nat) (A : 'M[R]_n).
+Implicit Types p q : {poly R}.

-Definition char_poly_mx := 'X%:M - map_mx (@polyC R) A.
-Definition char_poly := \det char_poly_mx.
+Definition char_poly_mx := 'X%:M - map_mx (@polyC R) A.
+Definition char_poly := \det char_poly_mx.

-Let diagA := [seq A i i | i : 'I_n].
-Let size_diagA : size diagA = n.
+Let diagA := [seq A i i | i : 'I_n].
+Let size_diagA : size diagA = n.

Let split_diagA :
-  exists2 q, \prod_(x <- diagA) ('X - x%:P) + q = char_poly & size q ≤ n.-1.
+  exists2 q, \prod_(x <- diagA) ('X - x%:P) + q = char_poly & size q ≤ n.-1.

-Lemma size_char_poly : size char_poly = n.+1.
+Lemma size_char_poly : size char_poly = n.+1.

-Lemma char_poly_monic : char_poly \is monic.
+Lemma char_poly_monic : char_poly \is monic.

-Lemma char_poly_trace : n > 0 → char_poly`_n.-1 = - \tr A.
+Lemma char_poly_trace : n > 0 → char_poly`_n.-1 = - \tr A.

-Lemma char_poly_det : char_poly`_0 = (- 1) ^+ n × \det A.
+Lemma char_poly_det : char_poly`_0 = (- 1) ^+ n × \det A.

End CharPoly.

-Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) :
-  ∃ phi : {rmorphism 'M[{poly R}]_n → {poly 'M[R]_n}},
-  [/\ bijective phi,
-      ∀ p, phi p%:M = map_poly scalar_mx p,
-      ∀ A, phi (map_mx polyC A) = A%:P
-    & ∀ A i j k, (phi A)`_k i j = (A i j)`_k].

-Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) :
-  horner_mx A (char_poly A) = 0.
+Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) :
+  ∃ phi : {rmorphism 'M[{poly R}]_n → {poly 'M[R]_n}},
+  [/\ bijective phi,
+      ∀ p, phi p%:M = map_poly scalar_mx p,
+      ∀ A, phi (map_mx polyC A) = A%:P
+    & ∀ A i j k, (phi A)`_k i j = (A i j)`_k].
+ +
+Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) :
+  horner_mx A (char_poly A) = 0.
+ +
+Lemma eigenvalue_root_char (F : fieldType) n (A : 'M[F]_n) a :
+  eigenvalue A a = root (char_poly A) a.
+ +
+Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) :=
+  \matrix_(i < d, j < d)
+    if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R.

-Lemma eigenvalue_root_char (F : fieldType) n (A : 'M[F]_n) a :
-  eigenvalue A a = root (char_poly A) a.
+Lemma companionmxK {R : comRingType} (p : {poly R}) :
+   p \is monic → char_poly (companionmx p) = p.
+ +
+Lemma mulmx_delta_companion (R : ringType) (p : seq R)
+  (i: 'I_(size p).-1) (i_small : i.+1 < (size p).-1):
+  delta_mx 0 i ×m companionmx p = delta_mx 0 (Ordinal i_small) :> 'rV__.

Section MinPoly.

-Variables (F : fieldType) (n' : nat).
-Variable A : 'M[F]_n.
-Implicit Types p q : {poly F}.
+Variables (F : fieldType) (n' : nat).
+Variable A : 'M[F]_n.
+Implicit Types p q : {poly F}.

-Fact degree_mxminpoly_proof : ∃ d, \rank (powers_mx A d.+1) ≤ d.
+Fact degree_mxminpoly_proof : ∃ d, \rank (powers_mx A d.+1) ≤ d.
Definition degree_mxminpoly := ex_minn degree_mxminpoly_proof.

-Lemma mxminpoly_nonconstant : d > 0.
+Lemma mxminpoly_nonconstant : d > 0.

-Lemma minpoly_mx1 : (1%:M \in Ad)%MS.
+Lemma minpoly_mx1 : (1%:M \in Ad)%MS.

Lemma minpoly_mx_free : row_free Ad.

-Lemma horner_mx_mem p : (horner_mx A p \in Ad)%MS.
+Lemma horner_mx_mem p : (horner_mx A p \in Ad)%MS.

-Definition mx_inv_horner B := rVpoly (mxvec B ×m pinvmx Ad).
+Definition mx_inv_horner B := rVpoly (mxvec B ×m pinvmx Ad).

-Lemma mx_inv_horner0 : mx_inv_horner 0 = 0.
+Lemma mx_inv_horner0 : mx_inv_horner 0 = 0.

-Lemma mx_inv_hornerK B : (B \in Ad)%MS → horner_mx A (mx_inv_horner B) = B.
+Lemma mx_inv_hornerK B : (B \in Ad)%MS → horner_mx A (mx_inv_horner B) = B.

-Lemma minpoly_mxM B C : (B \in Ad → C \in Ad → B × C \in Ad)%MS.
+Lemma minpoly_mxM B C : (B \in Ad → C \in Ad → B × C \in Ad)%MS.

Lemma minpoly_mx_ring : mxring Ad.

-Definition mxminpoly := 'X^d - mx_inv_horner (A ^+ d).
+Definition mxminpoly := 'X^d - mx_inv_horner (A ^+ d).

-Lemma size_mxminpoly : size p_A = d.+1.
+Lemma size_mxminpoly : size p_A = d.+1.

-Lemma mxminpoly_monic : p_A \is monic.
+Lemma mxminpoly_monic : p_A \is monic.

-Lemma size_mod_mxminpoly p : size (p %% p_A) ≤ d.
+Lemma size_mod_mxminpoly p : size (p %% p_A) ≤ d.

-Lemma mx_root_minpoly : horner_mx A p_A = 0.
+Lemma mx_root_minpoly : horner_mx A p_A = 0.

-Lemma horner_rVpolyK (u : 'rV_d) :
-  mx_inv_horner (horner_mx A (rVpoly u)) = rVpoly u.
+Lemma horner_rVpolyK (u : 'rV_d) :
+  mx_inv_horner (horner_mx A (rVpoly u)) = rVpoly u.

-Lemma horner_mxK p : mx_inv_horner (horner_mx A p) = p %% p_A.
+Lemma horner_mxK p : mx_inv_horner (horner_mx A p) = p %% p_A.

-Lemma mxminpoly_min p : horner_mx A p = 0 → p_A %| p.
+Lemma mxminpoly_min p : horner_mx A p = 0 → p_A %| p.

-Lemma horner_rVpoly_inj : @injective 'M_n 'rV_d (horner_mx A \o rVpoly).
+Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d → 'M_n).

-Lemma mxminpoly_linear_is_scalar : (d ≤ 1) = is_scalar_mx A.
+Lemma mxminpoly_linear_is_scalar : (d ≤ 1) = is_scalar_mx A.

-Lemma mxminpoly_dvd_char : p_A %| char_poly A.
+Lemma mxminpoly_dvd_char : p_A %| char_poly A.

-Lemma eigenvalue_root_min a : eigenvalue A a = root p_A a.
+Lemma eigenvalue_root_min a : eigenvalue A a = root p_A a.

End MinPoly.
+
+ +
+
@@ -343,20 +367,20 @@ Section MapRingMatrix.

-Variables (aR rR : ringType) (f : {rmorphism aR → rR}).
-Variables (d n : nat) (A : 'M[aR]_n).
+Variables (aR rR : ringType) (f : {rmorphism aR → rR}).
+Variables (d n : nat) (A : 'M[aR]_n).

-Lemma map_rVpoly (u : 'rV_d) : fp (rVpoly u) = rVpoly u^f.
+Lemma map_rVpoly (u : 'rV_d) : fp (rVpoly u) = rVpoly u^f.

-Lemma map_poly_rV p : (poly_rV p)^f = poly_rV (fp p) :> 'rV_d.
+Lemma map_poly_rV p : (poly_rV p)^f = poly_rV (fp p) :> 'rV_d.

-Lemma map_char_poly_mx : map_mx fp (char_poly_mx A) = char_poly_mx A^f.
+Lemma map_char_poly_mx : map_mx fp (char_poly_mx A) = char_poly_mx A^f.

-Lemma map_char_poly : fp (char_poly A) = char_poly A^f.
+Lemma map_char_poly : fp (char_poly A) = char_poly A^f.

End MapRingMatrix.
@@ -365,9 +389,9 @@ Section MapResultant.

-Lemma map_resultant (aR rR : ringType) (f : {rmorphism {poly aR} → rR}) p q :
-    f (lead_coef p) != 0 → f (lead_coef q) != 0 →
-  f (resultant p q)= resultant (map_poly f p) (map_poly f q).
+Lemma map_resultant (aR rR : ringType) (f : {rmorphism {poly aR} → rR}) p q :
+    f (lead_coef p) != 0 → f (lead_coef q) != 0 →
+  f (resultant p q)= resultant (map_poly f p) (map_poly f q).

End MapResultant.
@@ -376,14 +400,14 @@ Section MapComRing.

-Variables (aR rR : comRingType) (f : {rmorphism aR → rR}).
-Variables (n' : nat) (A : 'M[aR]_n'.+1).
+Variables (aR rR : comRingType) (f : {rmorphism aR → rR}).
+Variables (n' : nat) (A : 'M[aR]_n'.+1).

-Lemma map_powers_mx e : (powers_mx A e)^f = powers_mx A^f e.
+Lemma map_powers_mx e : (powers_mx A e)^f = powers_mx A^f e.

-Lemma map_horner_mx p : (horner_mx A p)^f = horner_mx A^f (fp p).
+Lemma map_horner_mx p : (horner_mx A p)^f = horner_mx A^f (fp p).

End MapComRing.
@@ -392,17 +416,25 @@ Section MapField.

-Variables (aF rF : fieldType) (f : {rmorphism aF → rF}).
-Variables (n' : nat) (A : 'M[aF]_n'.+1).
+Variables (aF rF : fieldType) (f : {rmorphism aF → rF}).
+Variables (n' : nat) (A : 'M[aF]_n'.+1) (p : {poly aF}).
+ +
+Lemma map_mx_companion (e := congr1 predn (size_map_poly _ _)) :
+  (companionmx p)^f = castmx (e, e) (companionmx (fp p)).

-Lemma degree_mxminpoly_map : degree_mxminpoly A^f = degree_mxminpoly A.
+Lemma companion_map_poly (e := esym (congr1 predn (size_map_poly _ _))) :
+  companionmx (fp p) = castmx (e, e) (companionmx p)^f.
+ +
+Lemma degree_mxminpoly_map : degree_mxminpoly A^f = degree_mxminpoly A.

-Lemma mxminpoly_map : mxminpoly A^f = fp (mxminpoly A).
+Lemma mxminpoly_map : mxminpoly A^f = fp (mxminpoly A).

-Lemma map_mx_inv_horner u : fp (mx_inv_horner A u) = mx_inv_horner A^f u^f.
+Lemma map_mx_inv_horner u : fp (mx_inv_horner A u) = mx_inv_horner A^f u^f.

End MapField.
@@ -411,24 +443,24 @@ Section IntegralOverRing.

-Definition integralOver (R K : ringType) (RtoK : R → K) (z : K) :=
-  exists2 p, p \is monic & root (map_poly RtoK p) z.
+Definition integralOver (R K : ringType) (RtoK : R → K) (z : K) :=
+  exists2 p, p \is monic & root (map_poly RtoK p) z.

Definition integralRange R K RtoK := ∀ z, @integralOver R K RtoK z.

-Variables (B R K : ringType) (BtoR : B → R) (RtoK : {rmorphism R → K}).
+Variables (B R K : ringType) (BtoR : B → R) (RtoK : {rmorphism R → K}).

Lemma integral_rmorph x :
-  integralOver BtoR x → integralOver (RtoK \o BtoR) (RtoK x).
+  integralOver BtoR x → integralOver (RtoK \o BtoR) (RtoK x).

Lemma integral_id x : integralOver RtoK (RtoK x).

-Lemma integral_nat n : integralOver RtoK n%:R.
+Lemma integral_nat n : integralOver RtoK n%:R.

Lemma integral0 : integralOver RtoK 0.
@@ -437,8 +469,8 @@ Lemma integral1 : integralOver RtoK 1.

-Lemma integral_poly (p : {poly K}) :
-  (∀ i, integralOver RtoK p`_i) ↔ {in p : seq K, integralRange RtoK}.
+Lemma integral_poly (p : {poly K}) :
+  (∀ i, integralOver RtoK p`_i) ↔ {in p : seq K, integralRange RtoK}.

End IntegralOverRing.
@@ -447,46 +479,46 @@ Section IntegralOverComRing.

-Variables (R K : comRingType) (RtoK : {rmorphism R → K}).
+Variables (R K : comRingType) (RtoK : {rmorphism R → K}).

-Lemma integral_horner_root w (p q : {poly K}) :
-    p \is monic → root p w →
-    {in p : seq K, integralRange RtoK} → {in q : seq K, integralRange RtoK} →
-  integralOver RtoK q.[w].
+Lemma integral_horner_root w (p q : {poly K}) :
+    p \is monic → root p w →
+    {in p : seq K, integralRange RtoK} → {in q : seq K, integralRange RtoK} →
+  integralOver RtoK q.[w].

Lemma integral_root_monic u p :
-    p \is monic → root p u → {in p : seq K, integralRange RtoK} →
+    p \is monic → root p u → {in p : seq K, integralRange RtoK} →
  integralOver RtoK u.

-Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K).
+Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core.

-Let XsubC0 (u : K) : root ('X - u%:P) u.
+Let XsubC0 (u : K) : root ('X - u%:P) u.
Let intR_XsubC u :
-  integralOver RtoK (- u) → {in 'X - u%:P : seq K, integralRange RtoK}.
+  integralOver RtoK (- u) → {in 'X - u%:P : seq K, integralRange RtoK}.

-Lemma integral_opp u : integralOver RtoK u → integralOver RtoK (- u).
+Lemma integral_opp u : integralOver RtoK u → integralOver RtoK (- u).

-Lemma integral_horner (p : {poly K}) u :
-    {in p : seq K, integralRange RtoK} → integralOver RtoK u →
-  integralOver RtoK p.[u].
+Lemma integral_horner (p : {poly K}) u :
+    {in p : seq K, integralRange RtoK} → integralOver RtoK u →
+  integralOver RtoK p.[u].

Lemma integral_sub u v :
-  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u - v).
+  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u - v).

Lemma integral_add u v :
-  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u + v).
+  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u + v).

Lemma integral_mul u v :
-  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u × v).
+  integralOver RtoK u → integralOver RtoK v → integralOver RtoK (u × v).

End IntegralOverComRing.
@@ -495,17 +527,17 @@ Section IntegralOverField.

-Variables (F E : fieldType) (FtoE : {rmorphism F → E}).
+Variables (F E : fieldType) (FtoE : {rmorphism F → E}).

-Definition algebraicOver (fFtoE : F → E) u :=
-  exists2 p, p != 0 & root (map_poly fFtoE p) u.
+Definition algebraicOver (fFtoE : F → E) u :=
+  exists2 p, p != 0 & root (map_poly fFtoE p) u.

-Notation mk_mon p := ((lead_coef p)^-1 *: p).
+Notation mk_mon p := ((lead_coef p)^-1 *: p).

-Lemma integral_algebraic u : algebraicOver FtoE u ↔ integralOver FtoE u.
+Lemma integral_algebraic u : algebraicOver FtoE u ↔ integralOver FtoE u.

Lemma algebraic_id a : algebraicOver FtoE (FtoE a).
@@ -517,37 +549,37 @@ Lemma algebraic1 : algebraicOver FtoE 1.

-Lemma algebraic_opp x : algebraicOver FtoE x → algebraicOver FtoE (- x).
+Lemma algebraic_opp x : algebraicOver FtoE x → algebraicOver FtoE (- x).

Lemma algebraic_add x y :
-  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x + y).
+  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x + y).

Lemma algebraic_sub x y :
-  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x - y).
+  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x - y).

Lemma algebraic_mul x y :
-  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x × y).
+  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x × y).

-Lemma algebraic_inv u : algebraicOver FtoE u → algebraicOver FtoE u^-1.
+Lemma algebraic_inv u : algebraicOver FtoE u → algebraicOver FtoE u^-1.

Lemma algebraic_div x y :
-  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x / y).
+  algebraicOver FtoE x → algebraicOver FtoE y → algebraicOver FtoE (x / y).

-Lemma integral_inv x : integralOver FtoE x → integralOver FtoE x^-1.
+Lemma integral_inv x : integralOver FtoE x → integralOver FtoE x^-1.

Lemma integral_div x y :
-  integralOver FtoE x → integralOver FtoE y → integralOver FtoE (x / y).
+  integralOver FtoE x → integralOver FtoE y → integralOver FtoE (x / y).

Lemma integral_root p u :
-    p != 0 → root p u → {in p : seq E, integralRange FtoE} →
+    p != 0 → root p u → {in p : seq E, integralRange FtoE} →
  integralOver FtoE u.

@@ -575,73 +607,73 @@

-Definition eval_mx (e : seq F) := map_mx (eval e).
+Definition eval_mx (e : seq F) := @map_mx term F (eval e).

-Definition mx_term := map_mx (@GRing.Const F).
+Definition mx_term := @map_mx F term GRing.Const.

-Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A.
+Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A.

-Definition mulmx_term m n p (A : 'M[term]_(m, n)) (B : 'M_(n, p)) :=
-  \matrix_(i, k) (\big[Add/0]_j (A i j × B j k))%T.
+Definition mulmx_term m n p (A : 'M[term]_(m, n)) (B : 'M_(n, p)) :=
+  \matrix_(i, k) (\big[Add/0]_j (A i j × B j k))%T.

-Lemma eval_mulmx e m n p (A : 'M[term]_(m, n)) (B : 'M_(n, p)) :
-  eval_mx e (mulmx_term A B) = eval_mx e A ×m eval_mx e B.
+Lemma eval_mulmx e m n p (A : 'M[term]_(m, n)) (B : 'M_(n, p)) :
+  eval_mx e (mulmx_term A B) = eval_mx e A ×m eval_mx e B.


-Let Schur m n (A : 'M[term]_(1 + m, 1 + n)) (a := A 0 0) :=
-  \matrix_(i, j) (drsubmx A i j - a^-1 × dlsubmx A i 0%R × ursubmx A 0%R j)%T.
+Let Schur m n (A : 'M[term]_(1 + m, 1 + n)) (a := A 0 0) :=
+  \matrix_(i, j) (drsubmx A i j - a^-1 × dlsubmx A i 0%R × ursubmx A 0%R j)%T.

-Fixpoint mxrank_form (r m n : nat) : 'M_(m, n) → form :=
-  match m, n return 'M_(m, n) → form with
-  | m'.+1, n'.+1 ⇒ fun A : 'M_(1 + m', 1 + n') ⇒
-    let nzA k := A k.1 k.2 != 0 in
-    let xSchur k := Schur (xrow k.1 0%R (xcol k.2 0%R A)) in
-    let recf k := Bool (r > 0) ∧ mxrank_form r.-1 (xSchur k) in
-    GRing.Pick nzA recf (Bool (r == 0%N))
-  | _, _ ⇒ fun _ ⇒ Bool (r == 0%N)
+Fixpoint mxrank_form (r m n : nat) : 'M_(m, n) → form :=
+  match m, n return 'M_(m, n) → form with
+  | m'.+1, n'.+1 ⇒ fun A : 'M_(1 + m', 1 + n') ⇒
+    let nzA k := A k.1 k.2 != 0 in
+    let xSchur k := Schur (xrow k.1 0%R (xcol k.2 0%R A)) in
+    let recf k := Bool (r > 0) ∧ mxrank_form r.-1 (xSchur k) in
+    GRing.Pick nzA recf (Bool (r == 0%N))
+  | _, _ ⇒ fun _ ⇒ Bool (r == 0%N)
  end%T.

-Lemma mxrank_form_qf r m n (A : 'M_(m, n)) : qf_form (mxrank_form r A).
+Lemma mxrank_form_qf r m n (A : 'M_(m, n)) : qf_form (mxrank_form r A).

-Lemma eval_mxrank e r m n (A : 'M_(m, n)) :
-  qf_eval e (mxrank_form r A) = (\rank (eval_mx e A) == r).
+Lemma eval_mxrank e r m n (A : 'M_(m, n)) :
+  qf_eval e (mxrank_form r A) = (\rank (eval_mx e A) == r).

-Lemma eval_vec_mx e m n (u : 'rV_(m × n)) :
-  eval_mx e (vec_mx u) = vec_mx (eval_mx e u).
+Lemma eval_vec_mx e m n (u : 'rV_(m × n)) :
+  eval_mx e (vec_mx u) = vec_mx (eval_mx e u).

-Lemma eval_mxvec e m n (A : 'M_(m, n)) :
-  eval_mx e (mxvec A) = mxvec (eval_mx e A).
+Lemma eval_mxvec e m n (A : 'M_(m, n)) :
+  eval_mx e (mxvec A) = mxvec (eval_mx e A).

Section Subsetmx.

-Variables (m1 m2 n : nat) (A : 'M[term]_(m1, n)) (B : 'M[term]_(m2, n)).
+Variables (m1 m2 n : nat) (A : 'M[term]_(m1, n)) (B : 'M[term]_(m2, n)).

Definition submx_form :=
-  \big[And/True]_(r < n.+1) (mxrank_form r (col_mx A B) ==> mxrank_form r B)%T.
+  \big[And/True]_(r < n.+1) (mxrank_form r (col_mx A B) ==> mxrank_form r B)%T.

Lemma eval_col_mx e :
-  eval_mx e (col_mx A B) = col_mx (eval_mx e A) (eval_mx e B).
+  eval_mx e (col_mx A B) = col_mx (eval_mx e A) (eval_mx e B).

Lemma submx_form_qf : qf_form submx_form.

-Lemma eval_submx e : qf_eval e submx_form = (eval_mx e A ≤ eval_mx e B)%MS.
+Lemma eval_submx e : qf_eval e submx_form = (eval_mx e A ≤ eval_mx e B)%MS.

End Subsetmx.
@@ -650,38 +682,38 @@ Section Env.

-Variable d : nat.
+Variable d : nat.

-Definition seq_of_rV (v : 'rV_d) : seq F := fgraph [ffun i ⇒ v 0 i].
+Definition seq_of_rV (v : 'rV_d) : seq F := fgraph [ffun i ⇒ v 0 i].

-Lemma size_seq_of_rV v : size (seq_of_rV v) = d.
+Lemma size_seq_of_rV v : size (seq_of_rV v) = d.

-Lemma nth_seq_of_rV x0 v (i : 'I_d) : nth x0 (seq_of_rV v) i = v 0 i.
+Lemma nth_seq_of_rV x0 v (i : 'I_d) : nth x0 (seq_of_rV v) i = v 0 i.

-Definition row_var k : 'rV[term]_d := \row_i ('X_(k × d + i))%T.
+Definition row_var k : 'rV[term]_d := \row_i ('X_(k × d + i))%T.

-Definition row_env (e : seq 'rV_d) := flatten (map seq_of_rV e).
+Definition row_env (e : seq 'rV_d) := flatten (map seq_of_rV e).

-Lemma nth_row_env e k (i : 'I_d) : (row_env e)`_(k × d + i) = e`_k 0 i.
+Lemma nth_row_env e k (i : 'I_d) : (row_env e)`_(k × d + i) = e`_k 0 i.

-Lemma eval_row_var e k : eval_mx (row_env e) (row_var k) = e`_k :> 'rV_d.
+Lemma eval_row_var e k : eval_mx (row_env e) (row_var k) = e`_k :> 'rV_d.

Definition Exists_row_form k (f : form) :=
-  foldr GRing.Exists f (codom (fun i : 'I_d ⇒ k × d + i)%N).
+  foldr GRing.Exists f (codom (fun i : 'I_d ⇒ k × d + i)%N).

Lemma Exists_rowP e k f :
-  d > 0 →
-   ((∃ v : 'rV[F]_d, holds (row_env (set_nth 0 e k v)) f)
-      ↔ holds (row_env e) (Exists_row_form k f)).
+  d > 0 →
+   ((∃ v : 'rV[F]_d, holds (row_env (set_nth 0 e k v)) f)
+      ↔ holds (row_env e) (Exists_row_form k f)).

End Env.
-- cgit v1.2.3