aeval_primPart_eq_zero — Mathlib

English

Let p ∈ R[X] with p ≠ 0, s ∈ S, and suppose aeval s p = 0 in S. Then aeval s p.primPart = 0.

Русский

Пусть p ∈ R[X], p ≠ 0, и s ∈ S, и если 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 aeval_primPart_eq_zero {S : Type*} [Ring S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : R[X]}
    {s : S} (hpzero : p ≠ 0) (hp : aeval s p = 0) : aeval s p.primPart = 0 :=
  by
  rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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