integerNormalization — Mathlib

English

The polynomial integerNormalization(M,p) is the polynomial over R whose coefficients are the coeffIntegerNormalization M p i, placed at the corresponding powers.

Русский

Полином integerNormalization(M,p) — полином над R, чьи коэффициенты равны coeffIntegerNormalization M p i на соответствующих степенях.

LaTeX

$$$\text{integerNormalization }(M,p) = \sum_{i \in \mathrm{supp}(p)} (\text{coeffIntegerNormalization }(M,p,i)) x^i$$$

Lean4

/-- `integerNormalization g` normalizes `g` to have integer coefficients
by clearing the denominators -/
noncomputable def integerNormalization (p : S[X]) : R[X] :=
  ∑ i ∈ p.support, monomial i (coeffIntegerNormalization M p i)

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