integerNormalization_eval₂_eq_zero

English

For polynomial p over K, integerNormalization is zero if and only if p is zero.

Русский

Для полинома p над K нормализация целиком обращается в ноль тогда и только тогда, когда p ноль.

LaTeX

$$$\text{integerNormalization }(M,p) = 0 \iff p = 0$$$

Lean4

theorem integerNormalization_eval₂_eq_zero (g : S →+* R') (p : S[X]) {x : R'} (hx : eval₂ g x p = 0) :
    eval₂ (g.comp (algebraMap R S)) x (integerNormalization M p) = 0 :=
  let ⟨b, hb⟩ := integerNormalization_map_to_map M p
  _root_.trans (eval₂_map (algebraMap R S) g x).symm
    (by rw [hb, ← IsScalarTower.algebraMap_smul S (b : R) p, eval₂_smul, hx, mul_zero])

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