integralNormalization_aeval_eq_zero

English

Under an algebra structure, if aeval z f = 0, then aeval(algebraMap f.leadingCoeff * z)(integralNormalization f) = 0.

Русский

При алгебраической структуре, если aeval z f = 0, тогда aeval(algebraMap f.leadingCoeff · z)(integralNormalization f) = 0.

LaTeX

$$$\mathrm{aeval}_{z} f = 0 \Rightarrow \mathrm{aeval}_{(\text{algebraMap } S A)(f.leadingCoeff) \cdot z}(\operatorname{integralNormalization} f) = 0$$$

Lean4

theorem integralNormalization_aeval_eq_zero [Algebra S A] {f : S[X]} {z : A} (hz : aeval z f = 0)
    (inj : ∀ x : S, algebraMap S A x = 0 → x = 0) :
    aeval (algebraMap S A f.leadingCoeff * z) (integralNormalization f) = 0 :=
  integralNormalization_eval₂_eq_zero_of_commute (algebraMap S A) hz (Algebra.commute_algebraMap_left _ _)
    (.map (.all _ _) _) inj

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