Library Combi.MPoly.antisym: Antisymmetric polynomials and Vandermonde product
Antisymmetric polynomials
- mpart s == the multi-monomial whose exponent are s if size s is smaller than the number of variables.
- partm m == the partition obtained by sorting the exponent of m.
- m \is dominant == the exponent of m are sorted in reverse order.
- p \is antisym == p is an antisymmetric polynomial. This is a keyed predicate closed by submodule operations submodPred.
- alternpol f == the alternating sunm of the permuted of f.
- rho == the multi-monomial [n-1, n-2, ..., 1, 0]
- Vanprod n R == the Vandermonde product in {mpoly R[n]}, that is the product
\prod_(i < j) ('X_i - 'X_j). - antim s == the n x n - matrix whose (i, j) coefficient is
'X_i^(s j - rho j) - Vanmx == the Vandermonde matrix
'X_i^(n - 1 - j) = 'X_i^(rho j). - Vandet == the Vandermonde determinant
- Vanprod_alt : Vanprod = alternpol 'X_[(rho n)]
- Vandet_VanprodE : Vandet = Vanprod
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint fingroup perm zmodp binomial.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import tools permcomp presentSn sorted partition.
Set Implicit Arguments.
Import LeqGeqOrder.
#[local] Reserved Notation "''a_' k"
(at level 8, k at level 2, format "''a_' k").
#[local] Reserved Notation "m # s"
(at level 40, left associativity, format "m # s").
#[local] Notation "''II_' n" := ('I_n * 'I_n)%type (at level 8, n at level 2).
Open Scope group_scope.
Open Scope nat_scope.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint fingroup perm zmodp binomial.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import tools permcomp presentSn sorted partition.
Set Implicit Arguments.
Import LeqGeqOrder.
#[local] Reserved Notation "''a_' k"
(at level 8, k at level 2, format "''a_' k").
#[local] Reserved Notation "m # s"
(at level 40, left associativity, format "m # s").
#[local] Notation "''II_' n" := ('I_n * 'I_n)%type (at level 8, n at level 2).
Open Scope group_scope.
Open Scope nat_scope.
Section MonomPart.
Variable n : nat.
Implicit Type m : 'X_{1.. n}.
Definition dominant : qualifier 0 'X_{1.. n} :=
[qualify m : 'X_{1.. n} | sorted geq m].
Definition mpart (s : seq nat) :=
if size s <= n then [multinom (nth 0 s i)%N | i < n] else mnm0.
Lemma dominant_eq m1 m2 :
m1 \is dominant -> m2 \is dominant -> perm_eq m1 m2 -> m1 = m2.
Fact partmP m : is_part (sort geq [seq d <- m | d != 0]).
Definition partm m := locked (IntPart (partmP m)).
Lemma partmE m : partm m = sort geq [seq d <- m | d != 0] :> seq nat.
Lemma size_partm m : size (partm m) <= n.
Lemma mpart_is_dominant sh : is_part sh -> mpart sh \is dominant.
Lemma is_dominant_partm m :
m \is dominant -> partm m = [seq d <- m | d != 0] :> seq nat.
Lemma is_dominant_nth_partm m (i : 'I_n) :
m \is dominant -> nth 0 (partm m) i = m i.
Lemma partmK m : m \is dominant -> mpart (partm m) = m.
Lemma mpartK sh :
is_part sh -> size sh <= n -> partm (mpart sh) = sh :> seq nat.
Lemma mpartE s i : size s <= n -> mpart s i = nth 0 s i.
Lemma mpart0 : @mpart [::] = 0%MM.
Lemma perm_mpart s1 s2 : perm_eq s1 s2 -> perm_eq (mpart s1) (mpart s2).
Lemma perm_partm m1 m2 : perm_eq m1 m2 -> partm m1 = partm m2.
Lemma partm_permK m : perm_eq m (mpart (partm m)).
Lemma sumn_mpart sh : size sh <= n -> sumn (mpart sh) = sumn sh.
Lemma mdeg_mpart sh : size sh <= n -> mdeg (mpart sh) = sumn sh.
Lemma sumn_partm m : sumn (partm m) = mdeg m.
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma mnm_perm m1 m2 : perm_eq m1 m2 -> {s : 'S_n | m1 == m2 # s}.
Lemma perm_mpart_partm m : {s : 'S_n | (mpart (partm m)) # s == m}.
Lemma mpart_partm_perm m : {s : 'S_n | (mpart (partm m)) == m # s}.
End MonomPart.
Arguments mpart [n] s.
Arguments dominant {n}.
Import GRing.Theory.
#[local] Open Scope ring_scope.
#[local] Definition simplexp := (expr0, expr1, scale1r, scaleN1r,
mulrN, mulNr, mulrNN).
Variable n : nat.
Implicit Type m : 'X_{1.. n}.
Definition dominant : qualifier 0 'X_{1.. n} :=
[qualify m : 'X_{1.. n} | sorted geq m].
Definition mpart (s : seq nat) :=
if size s <= n then [multinom (nth 0 s i)%N | i < n] else mnm0.
Lemma dominant_eq m1 m2 :
m1 \is dominant -> m2 \is dominant -> perm_eq m1 m2 -> m1 = m2.
Fact partmP m : is_part (sort geq [seq d <- m | d != 0]).
Definition partm m := locked (IntPart (partmP m)).
Lemma partmE m : partm m = sort geq [seq d <- m | d != 0] :> seq nat.
Lemma size_partm m : size (partm m) <= n.
Lemma mpart_is_dominant sh : is_part sh -> mpart sh \is dominant.
Lemma is_dominant_partm m :
m \is dominant -> partm m = [seq d <- m | d != 0] :> seq nat.
Lemma is_dominant_nth_partm m (i : 'I_n) :
m \is dominant -> nth 0 (partm m) i = m i.
Lemma partmK m : m \is dominant -> mpart (partm m) = m.
Lemma mpartK sh :
is_part sh -> size sh <= n -> partm (mpart sh) = sh :> seq nat.
Lemma mpartE s i : size s <= n -> mpart s i = nth 0 s i.
Lemma mpart0 : @mpart [::] = 0%MM.
Lemma perm_mpart s1 s2 : perm_eq s1 s2 -> perm_eq (mpart s1) (mpart s2).
Lemma perm_partm m1 m2 : perm_eq m1 m2 -> partm m1 = partm m2.
Lemma partm_permK m : perm_eq m (mpart (partm m)).
Lemma sumn_mpart sh : size sh <= n -> sumn (mpart sh) = sumn sh.
Lemma mdeg_mpart sh : size sh <= n -> mdeg (mpart sh) = sumn sh.
Lemma sumn_partm m : sumn (partm m) = mdeg m.
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma mnm_perm m1 m2 : perm_eq m1 m2 -> {s : 'S_n | m1 == m2 # s}.
Lemma perm_mpart_partm m : {s : 'S_n | (mpart (partm m)) # s == m}.
Lemma mpart_partm_perm m : {s : 'S_n | (mpart (partm m)) == m # s}.
End MonomPart.
Arguments mpart [n] s.
Arguments dominant {n}.
Import GRing.Theory.
#[local] Open Scope ring_scope.
#[local] Definition simplexp := (expr0, expr1, scale1r, scaleN1r,
mulrN, mulNr, mulrNN).
Section ScalarChange.
Variables R S : ringType.
Variable mor : {rmorphism R -> S}.
Variable n : nat.
Lemma map_mpolyX (m : 'X_{1..n}) : map_mpoly mor 'X_[m] = 'X_[m].
Lemma msym_map_mpoly s (p : {mpoly R[n]}) :
msym s (map_mpoly mor p) = map_mpoly mor (msym s p).
End ScalarChange.
Variables R S : ringType.
Variable mor : {rmorphism R -> S}.
Variable n : nat.
Lemma map_mpolyX (m : 'X_{1..n}) : map_mpoly mor 'X_[m] = 'X_[m].
Lemma msym_map_mpoly s (p : {mpoly R[n]}) :
msym s (map_mpoly mor p) = map_mpoly mor (msym s p).
End ScalarChange.
Section MPolySym.
Variable n : nat.
Variable R : ringType.
Implicit Types p q r : {mpoly R[n]}.
Lemma issym_tpermP p :
reflect (forall i j, msym (tperm i j) p = p) (p \is symmetric).
Definition antisym : qualifier 0 {mpoly R[n]} :=
[qualify p | [forall s, msym s p == (-1) ^+ s *: p]].
Fact antisym_key : pred_key antisym.
Canonical antisym_keyed := KeyedQualifier antisym_key.
Lemma isantisymP p :
reflect (forall s, msym s p = (-1) ^+ s *: p) (p \is antisym).
Lemma isantisym_tpermP p :
reflect (forall i j, msym (tperm i j) p = if (i != j) then - p else p)
(p \is antisym).
Lemma antisym_char2 : (2 \in [char R]) -> symmetric =i antisym.
Lemma perm_smalln : n <= 1 -> forall s : 'S_n, s = 1%g.
Lemma sym_smalln : n <= 1 -> (@symmetric n R) =i predT.
Lemma antisym_smalln : n <= 1 -> antisym =i predT.
Lemma antisym_zmod : zmod_closed antisym.
Lemma antisym_submod_closed : submod_closed antisym.
Lemma sym_anti p q :
p \is antisym -> q \is symmetric -> p * q \is antisym.
Lemma anti_anti p q :
p \is antisym -> q \is antisym -> p * q \is symmetric.
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma isantisym_msupp p (s : 'S_n) (m : 'X_{1..n}) : p \is antisym ->
(m#s \in msupp p) = (m \in msupp p).
Import Order Order.Syntax Order.TotalTheory.
Lemma mlead_antisym_sorted (p : {mpoly R[n]}) : p \is antisym ->
forall (i j : 'I_n), i <= j -> (mlead p) j <= (mlead p) i.
End MPolySym.
Arguments antisym {n R}.
Lemma issym_eltrP n (R : ringType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = p) (p \is symmetric).
Lemma isantisym_eltrP n (R : ringType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = - p) (p \is antisym).
Variable n : nat.
Variable R : ringType.
Implicit Types p q r : {mpoly R[n]}.
Lemma issym_tpermP p :
reflect (forall i j, msym (tperm i j) p = p) (p \is symmetric).
Definition antisym : qualifier 0 {mpoly R[n]} :=
[qualify p | [forall s, msym s p == (-1) ^+ s *: p]].
Fact antisym_key : pred_key antisym.
Canonical antisym_keyed := KeyedQualifier antisym_key.
Lemma isantisymP p :
reflect (forall s, msym s p = (-1) ^+ s *: p) (p \is antisym).
Lemma isantisym_tpermP p :
reflect (forall i j, msym (tperm i j) p = if (i != j) then - p else p)
(p \is antisym).
Lemma antisym_char2 : (2 \in [char R]) -> symmetric =i antisym.
Lemma perm_smalln : n <= 1 -> forall s : 'S_n, s = 1%g.
Lemma sym_smalln : n <= 1 -> (@symmetric n R) =i predT.
Lemma antisym_smalln : n <= 1 -> antisym =i predT.
Lemma antisym_zmod : zmod_closed antisym.
Lemma antisym_submod_closed : submod_closed antisym.
Lemma sym_anti p q :
p \is antisym -> q \is symmetric -> p * q \is antisym.
Lemma anti_anti p q :
p \is antisym -> q \is antisym -> p * q \is symmetric.
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma isantisym_msupp p (s : 'S_n) (m : 'X_{1..n}) : p \is antisym ->
(m#s \in msupp p) = (m \in msupp p).
Import Order Order.Syntax Order.TotalTheory.
Lemma mlead_antisym_sorted (p : {mpoly R[n]}) : p \is antisym ->
forall (i j : 'I_n), i <= j -> (mlead p) j <= (mlead p) i.
End MPolySym.
Arguments antisym {n R}.
Lemma issym_eltrP n (R : ringType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = p) (p \is symmetric).
Lemma isantisym_eltrP n (R : ringType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = - p) (p \is antisym).
Definition alternpol n (R : ringType) (f : {mpoly R[n]}) : {mpoly R[n]} :=
\sum_(s : 'S_n) (-1) ^+ s *: msym s f.
Section AlternIDomain.
Variable n : nat.
Variable R : idomainType.
Hypothesis Hchar : ~~ (2 \in [char R]).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma sym_antisym_char_not2 :
n >= 2 -> forall p : {mpoly R[n]}, p \is symmetric -> p \is antisym -> p = 0.
Definition rho := [multinom (n - 1 - i)%N | i < n].
Lemma rho_iota : rho = rev (iota 0 n) :> seq nat.
Lemma rho_uniq : uniq rho.
Lemma mdeg_rho : mdeg rho = 'C(n, 2).
Lemma alt_homog : 'a_(rho) \is 'C(n, 2).-homog.
Lemma alt_anti m : 'a_m \is antisym.
\sum_(s : 'S_n) (-1) ^+ s *: msym s f.
Section AlternIDomain.
Variable n : nat.
Variable R : idomainType.
Hypothesis Hchar : ~~ (2 \in [char R]).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).
#[local] Notation "m # s" := [multinom m (s i) | i < n].
Lemma sym_antisym_char_not2 :
n >= 2 -> forall p : {mpoly R[n]}, p \is symmetric -> p \is antisym -> p = 0.
Definition rho := [multinom (n - 1 - i)%N | i < n].
Lemma rho_iota : rho = rev (iota 0 n) :> seq nat.
Lemma rho_uniq : uniq rho.
Lemma mdeg_rho : mdeg rho = 'C(n, 2).
Lemma alt_homog : 'a_(rho) \is 'C(n, 2).-homog.
Lemma alt_anti m : 'a_m \is antisym.
Section LeadingMonomial.
Variable p : {mpoly R[n]}.
Implicit Types q r : {mpoly R[n]}.
Hypothesis Hpn0 : p != 0.
Hypothesis Hpanti : p \is antisym.
Lemma sym_antiE q : (q \is symmetric) = (p * q \is antisym).
Lemma isantisym_msupp_uniq (m : 'X_{1..n}) : m \in msupp p -> uniq m.
Hypothesis Hphomog : p \is 'C(n , 2).-homog.
Lemma isantisym_mlead_iota : mlead p = rev (iota 0 n) :> seq nat.
Lemma isantisym_mlead_rho : mlead p = rho.
End LeadingMonomial.
Lemma isantisym_alt (p : {mpoly R[n]}) :
p != 0 -> p \is antisym -> p \is ('C(n, 2)).-homog -> p = p@_(rho) *: 'a_rho.
End AlternIDomain.
Variable p : {mpoly R[n]}.
Implicit Types q r : {mpoly R[n]}.
Hypothesis Hpn0 : p != 0.
Hypothesis Hpanti : p \is antisym.
Lemma sym_antiE q : (q \is symmetric) = (p * q \is antisym).
Lemma isantisym_msupp_uniq (m : 'X_{1..n}) : m \in msupp p -> uniq m.
Hypothesis Hphomog : p \is 'C(n , 2).-homog.
Lemma isantisym_mlead_iota : mlead p = rev (iota 0 n) :> seq nat.
Lemma isantisym_mlead_rho : mlead p = rho.
End LeadingMonomial.
Lemma isantisym_alt (p : {mpoly R[n]}) :
p != 0 -> p \is antisym -> p \is ('C(n, 2)).-homog -> p = p@_(rho) *: 'a_rho.
End AlternIDomain.
Definition Vanprod {n} {R : ringType} : {mpoly R[n]} :=
\prod_(p : 'II_n | p.1 < p.2) ('X_p.1 - 'X_p.2).
Section EltrP.
Variable n i : nat.
Implicit Type (p : 'II_n.+1).
#[local] Definition eltrp p := ('s_i p.1, 's_i p.2).
#[local] Definition predi p := (p.1 < p.2) && (p != (inord i, inord i.+1)).
Lemma eltrpK : involutive eltrp.
Lemma predi_eltrp p : i < n -> predi p -> predi (eltrp p).
Lemma predi_eltrpE p : i < n -> predi p = predi ('s_i p.1, 's_i p.2).
End EltrP.
Lemma Vanprod_anti n (R : comRingType) : @Vanprod n R \is antisym.
Lemma sym_VanprodM n (R : comRingType) (p : {mpoly R[n]}) :
p \is symmetric -> Vanprod * p \is antisym.
Section Vanprod.
Variable n : nat.
Variable R : comRingType.
#[local] Notation Delta := (@Vanprod n R).
#[local] Notation "'X_ i" := (@mpolyX n R U_(i)). #[local] Notation rho := (rho n).
#[local] Notation "''a_' k" := (alternpol 'X_[k]).
Lemma polyX_inj (i j : 'I_n) : 'X_i = 'X_j -> i = j.
Lemma diffX_neq0 (i j : 'I_n) : i != j -> 'X_i - 'X_j != 0.
Lemma msuppX1 i : msupp 'X_i = [:: U_(i)%MM].
Let abound b : {mpoly R[n]} :=
\prod_(p : 'II_n | p.1 < p.2 <= b) ('X_p.1 - 'X_p.2).
Let rbound b := [multinom (b - i)%N | i < n].
Lemma mesymlm_rbound b : (mesymlm n b <= rbound b)%MM.
Lemma coeffXdiff (b : 'I_n) (k : 'X_{1..n}) (i : 'I_n) :
(k <= rbound b)%MM -> ('X_i - 'X_b)@_k = (k == U_(i)%MM)%:R.
Lemma coeff_prodXdiff (b : 'I_n) (k : 'X_{1..n}) :
(k <= rbound b)%MM ->
(\prod_(i < n | i < b) ('X_i - 'X_b))@_k = (k == mesymlm n b)%:R.
Lemma mcoeff_arbound b : b < n -> (abound b)@_(rbound b) = 1.
Lemma Vanprod_coeff_rho : Delta@_rho = 1.
Corollary Vanprod_neq0 : Delta != 0.
Lemma Vanprod_dhomog : Delta \is 'C(n, 2).-homog.
End Vanprod.
Theorem Vanprod_alt_int n :
Vanprod = alternpol 'X_[rho n] :> {mpoly int[n]}.
Corollary Vanprod_alt n (R : ringType) :
Vanprod = alternpol 'X_[rho n] :> {mpoly R[n]}.
From mathcomp Require Import matrix.
\prod_(p : 'II_n | p.1 < p.2) ('X_p.1 - 'X_p.2).
Section EltrP.
Variable n i : nat.
Implicit Type (p : 'II_n.+1).
#[local] Definition eltrp p := ('s_i p.1, 's_i p.2).
#[local] Definition predi p := (p.1 < p.2) && (p != (inord i, inord i.+1)).
Lemma eltrpK : involutive eltrp.
Lemma predi_eltrp p : i < n -> predi p -> predi (eltrp p).
Lemma predi_eltrpE p : i < n -> predi p = predi ('s_i p.1, 's_i p.2).
End EltrP.
Lemma Vanprod_anti n (R : comRingType) : @Vanprod n R \is antisym.
Lemma sym_VanprodM n (R : comRingType) (p : {mpoly R[n]}) :
p \is symmetric -> Vanprod * p \is antisym.
Section Vanprod.
Variable n : nat.
Variable R : comRingType.
#[local] Notation Delta := (@Vanprod n R).
#[local] Notation "'X_ i" := (@mpolyX n R U_(i)). #[local] Notation rho := (rho n).
#[local] Notation "''a_' k" := (alternpol 'X_[k]).
Lemma polyX_inj (i j : 'I_n) : 'X_i = 'X_j -> i = j.
Lemma diffX_neq0 (i j : 'I_n) : i != j -> 'X_i - 'X_j != 0.
Lemma msuppX1 i : msupp 'X_i = [:: U_(i)%MM].
Let abound b : {mpoly R[n]} :=
\prod_(p : 'II_n | p.1 < p.2 <= b) ('X_p.1 - 'X_p.2).
Let rbound b := [multinom (b - i)%N | i < n].
Lemma mesymlm_rbound b : (mesymlm n b <= rbound b)%MM.
Lemma coeffXdiff (b : 'I_n) (k : 'X_{1..n}) (i : 'I_n) :
(k <= rbound b)%MM -> ('X_i - 'X_b)@_k = (k == U_(i)%MM)%:R.
Lemma coeff_prodXdiff (b : 'I_n) (k : 'X_{1..n}) :
(k <= rbound b)%MM ->
(\prod_(i < n | i < b) ('X_i - 'X_b))@_k = (k == mesymlm n b)%:R.
Lemma mcoeff_arbound b : b < n -> (abound b)@_(rbound b) = 1.
Lemma Vanprod_coeff_rho : Delta@_rho = 1.
Corollary Vanprod_neq0 : Delta != 0.
Lemma Vanprod_dhomog : Delta \is 'C(n, 2).-homog.
End Vanprod.
Theorem Vanprod_alt_int n :
Vanprod = alternpol 'X_[rho n] :> {mpoly int[n]}.
Corollary Vanprod_alt n (R : ringType) :
Vanprod = alternpol 'X_[rho n] :> {mpoly R[n]}.
From mathcomp Require Import matrix.
Section VandermondeDet.
Variable n : nat.
Variable R : comRingType.
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).
#[local] Notation rho := (rho n).
Definition antim (s : seq nat) : 'M[ {mpoly R[n]} ]_n :=
\matrix_(i, j < n) 'X_i ^+ (nth 0 s j + (n - 1) - j)%N.
Definition Vanmx : 'M[ {mpoly R[n]} ]_n :=
\matrix_(i, j < n) 'X_i ^+ (n - 1 - j).
Definition Vandet := \det Vanmx.
#[local] Open Scope ring_scope.
Lemma Vanmx_antimE : Vanmx = antim [::].
Lemma alt_detE s : 'a_(s + rho) = \det (antim s).
Corollary Vandet_VanprodE : Vandet = Vanprod.
Lemma mcoeff_alt (m : 'X_{1..n}) : uniq m -> ('a_m)@_m = 1.
Lemma alt_uniq_non0 (m : 'X_{1..n}) : uniq m -> 'a_m != 0.
Lemma alt_rho_non0 : 'a_rho != 0.
Lemma alt_alternate (m : 'X_{1..n}) (i j : 'I_n) :
i != j -> m i = m j -> 'a_m = 0.
Lemma alt_add1_0 (m : 'X_{1..n}) i :
(nth 0%N m i).+1 = nth 0%N m i.+1 -> 'a_(m + rho) = 0.
End VandermondeDet.
Variable n : nat.
Variable R : comRingType.
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).
#[local] Notation rho := (rho n).
Definition antim (s : seq nat) : 'M[ {mpoly R[n]} ]_n :=
\matrix_(i, j < n) 'X_i ^+ (nth 0 s j + (n - 1) - j)%N.
Definition Vanmx : 'M[ {mpoly R[n]} ]_n :=
\matrix_(i, j < n) 'X_i ^+ (n - 1 - j).
Definition Vandet := \det Vanmx.
#[local] Open Scope ring_scope.
Lemma Vanmx_antimE : Vanmx = antim [::].
Lemma alt_detE s : 'a_(s + rho) = \det (antim s).
Corollary Vandet_VanprodE : Vandet = Vanprod.
Lemma mcoeff_alt (m : 'X_{1..n}) : uniq m -> ('a_m)@_m = 1.
Lemma alt_uniq_non0 (m : 'X_{1..n}) : uniq m -> 'a_m != 0.
Lemma alt_rho_non0 : 'a_rho != 0.
Lemma alt_alternate (m : 'X_{1..n}) (i j : 'I_n) :
i != j -> m i = m j -> 'a_m = 0.
Lemma alt_add1_0 (m : 'X_{1..n}) i :
(nth 0%N m i).+1 = nth 0%N m i.+1 -> 'a_(m + rho) = 0.
End VandermondeDet.