integerNormalization_aeval_eq_zero

English

If aeval x p = 0 in S[X], then aeval x (integerNormalization M p) = 0 in R'[X] for any suitable target.

Русский

Если aeval x p = 0, то aeval x (integerNormalization M p) = 0 в целевой алгебре.

LaTeX

$$$\forall x, \ aeval(x, p) = 0 \Rightarrow aeval(x, \ text{integerNormalization }(M,p)) = 0$$$

Lean4

theorem integerNormalization_aeval_eq_zero [Algebra R R'] [Algebra S R'] [IsScalarTower R S R'] (p : S[X]) {x : R'}
    (hx : aeval x p = 0) : aeval x (integerNormalization M p) = 0 := by
  rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]

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