Weighted Gauss valuation (source code)

= Weighted Gauss valuation
{title2=$w_t(\sum_j a_jX^j)=\min_j(v(a_j)+jt)$}

For a <polynomial> over a <discretely valued field> and a rational weight $t$, this coefficient-minimum function is multiplicative. Scale the variable by an element of <valuation> $t$ in a valued extension and reduce the initial terms; nonzero residue polynomials have nonzero product. For a monic <polynomial> factored into roots, $w_t(f)=\sum_r\min(t,v(r))$. Its supporting lines determine the lower <Newton polygon>, giving the <Newton polygon root valuation theorem> and its multiplicities.