:: deftheorem Def7 defines Vandermonde POLYNOM8:def 8 :
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for m being Nat
for x being Element of L
for b₄ being Matrix of m,L holds
( b₄ = Vandermonde (x,m) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b₄ * (i,j) = pow (x,((i - 1) * (j - 1))) );