toFinsupp_inj

Mathlib.Algebra.Polynomial.Basic

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

English

For polynomials a, b, we have a.toFinsupp = b.toFinsupp if and only if a = b.

Русский

Для полиномов a, b верно: a.toFinsupp = b.toFinsupp тогда и только тогда, когда a = b.

LaTeX

$$$a^{\\wedge} = b^{\\wedge} \\iff a = b$$$

Lean4

@[simp]
theorem toFinsupp_inj {a b : R[X]} : a.toFinsupp = b.toFinsupp ↔ a = b :=
  toFinsupp_injective.eq_iff

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

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

Разделы

Аффилиация

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