toLaurent_inj

Mathlib.Algebra.Polynomial.Laurent

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

← MathLib Explorer

English

For polynomials f, g ∈ R[X], toLaurent f = toLaurent g if and only if f = g.

Русский

Для полиномов f, g ∈ R[X], toLaurent f = toLaurent g тогда и только тогда, когда f = g.

LaTeX

$$$\forall f,g \in R[X],\ toLaurent f = toLaurent g \iff f = g$$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_inj (f g : R[X]) : toLaurent f = toLaurent g ↔ f = g :=
  ⟨fun h => Polynomial.toLaurent_injective h, congr_arg _⟩

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

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

Разделы

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

Аффилиация

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