eval₂_primPart_eq_zero — Mathlib

English

Let S be a domain with an R-algebra structure. If hpzero: p ≠ 0 and hp: aeval s p = 0, then aeval s p.primPart = 0.

Русский

Пусть S — область, имеющая структуру алгебра над R. Если p ≠ 0 и aeval s p = 0, то aeval s p.primPart = 0.

LaTeX

$$$p \neq 0 \land aeval_s(p) = 0 \Rightarrow aeval_s(p.primPart) = 0$$$

Lean4

theorem eval₂_primPart_eq_zero {S : Type*} [CommSemiring S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective f)
    {p : R[X]} {s : S} (hpzero : p ≠ 0) (hp : eval₂ f s p = 0) : eval₂ f s p.primPart = 0 :=
  by
  rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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