taylor_eq_zero — Mathlib

English

For any r ∈ R and f ∈ R[X], taylor(r,f) = 0 if and only if f = 0. In particular, the Taylor shift taylor r is injective.

Русский

Для любого r ∈ R и f ∈ R[X] тaylor(r,f) = 0 тогда и только тогда, f = 0. Отображение ряда Тейлора инъективно.

LaTeX

$$$$ taylor(r,f) = 0 \\iff f = 0. $$$$

Lean4

@[simp]
theorem taylor_eq_zero : taylor r f = 0 ↔ f = 0 := by
  rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]

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