instValuedWithZeroMultiplicativeInt

English

Same as Monomial valuation: for any n and a ≠ 0, the valuation v(monomial n a) equals v(X)^n under trivial-on-constants assumption.

Русский

То же самое, что и оценка монома: для любых n и a ≠ 0 выполняется v(monomial n a) = v(X)^n при тривиальности на константах.

LaTeX

$$$\forall n\in\mathbb{N}, \forall a\in K\setminus\{0\},\quad v(\operatorname{monomial} n\ a) = v(\mathrm{X})^{n}$$$

Lean4

instance : Valued (RatFunc K) ℤᵐ⁰ :=
  Valued.mk' ((idealX K).valuation _)

Похожие утверждения