coeff_injective

Mathlib.Algebra.Polynomial.Basic

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

← MathLib Explorer

English

The map p ↦ coeff(p) is injective; i.e., if coeff(p) = coeff(q) then p = q.

Русский

Коэффициентная карта инъективна: если coeff(p) = coeff(q), то p = q.

LaTeX

$$$\forall p,q \in R[X],\; \mathrm{coeff}(p) = \mathrm{coeff}(q) \Rightarrow p = q$$$

Lean4

theorem coeff_injective : Injective (coeff : R[X] → ℕ → R) :=
  by
  rintro ⟨p⟩ ⟨q⟩
  simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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