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_boot order.
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_boot order.
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 : nzRingType.
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 : nzRingType.
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 : nzRingType.
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_pchar2 : (2 \in [pchar 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 : nzRingType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = p) (p \is symmetric).
Lemma isantisym_eltrP n (R : nzRingType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = - p) (p \is antisym).
Variable n : nat.
Variable R : nzRingType.
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_pchar2 : (2 \in [pchar 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 : nzRingType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = p) (p \is symmetric).
Lemma isantisym_eltrP n (R : nzRingType) (p : {mpoly R[n.+1]}) :
reflect (forall i, i < n -> msym 's_i p = - p) (p \is antisym).
Definition alternpol n (R : nzRingType) (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 [pchar 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 [pchar 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 : nzRingType} : {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 : comNzRingType) : @Vanprod n R \is antisym.
Lemma sym_VanprodM n (R : comNzRingType) (p : {mpoly R[n]}) :
p \is symmetric -> Vanprod * p \is antisym.
Section Vanprod.
Variable n : nat.
Variable R : comNzRingType.
#[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 : nzRingType) :
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 : comNzRingType) : @Vanprod n R \is antisym.
Lemma sym_VanprodM n (R : comNzRingType) (p : {mpoly R[n]}) :
p \is symmetric -> Vanprod * p \is antisym.
Section Vanprod.
Variable n : nat.
Variable R : comNzRingType.
#[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 : nzRingType) :
Vanprod = alternpol 'X_[rho n] :> {mpoly R[n]}.
From mathcomp Require Import matrix.
Section VandermondeDet.
Variable n : nat.
Variable R : comNzRingType.
#[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 : comNzRingType.
#[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.