integerNormalization_coeff — Mathlib

English

There exists b ∈ M such that for every i, there is a relation algebraMap R S (coeff of integerNormalization M p at i) equals b times p.coeff i.

Русский

Существует b ∈ M, такое что для каждого i коэффициент коэффициентов нормализации умножается на b в соответствующем отображении к S.

LaTeX

$$$\exists b \in M, \forall i, algebraMap_R_S( (integerNormalization M p)_{i} ) = (b : R) \cdot p_i$$$

Lean4

@[simp]
theorem integerNormalization_coeff (p : S[X]) (i : ℕ) :
    (integerNormalization M p).coeff i = coeffIntegerNormalization M p i := by
  simp +contextual [integerNormalization, coeff_monomial, coeffIntegerNormalization_of_coeff_zero]

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