English
Let R be a commutative ring and p ∈ R[X] be a non-zero-divisor in R[X]. Then the Taylor expansion of p about r, denoted taylor r p, is again a non-zero-divisor in R[X].
Русский
Пусть R — коммутативное кольцо, а p ∈ R[X] не является нулевым делителем в R[X]. Тогда разложение Тейлора p вокруг r, обозначаемое taylor r p, снова является ненулевым делителем в R[X].
LaTeX
$$$p \\in \\operatorname{nonZeroDivisors}(R[X]) \\Rightarrow \\operatorname{taylor}(r,p) \\in \\operatorname{nonZeroDivisors}(R[X]).$$$
Lean4
theorem taylor_mem_nonZeroDivisors (hp : p ∈ R[X]⁰) : taylor r p ∈ R[X]⁰ :=
by
rw [mem_nonZeroDivisors_iff_right]
intro x hx
have : x = taylor (r - r) x := by simp
rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul, LinearMap.map_eq_zero_iff _ (taylor_injective _),
mul_right_mem_nonZeroDivisors_eq_zero_iff hp, LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
