taylor_injective

Mathlib.Algebra.Polynomial.Taylor

URI: https://scilib.ai/kg/mathlib#Polynomial.taylor_injective

English

For any r ∈ R, the map p ↦ taylor(r,p) is injective on the polynomial ring R[X].

Русский

Для любого r ∈ R отображение p ↦ taylor(r,p) инъективно на кольце полиномов R[X].

LaTeX

$$$$ \\forall p,q \\in R[X],\\ taylor(r,p) = taylor(r,q) \\Rightarrow p=q. $$$$

Lean4

theorem taylor_injective (r : R) : Function.Injective (taylor r) :=
  (injective_iff_map_eq_zero' _).2 (taylor_eq_zero r)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru