trunc_toLaurent

Mathlib.Algebra.Polynomial.Laurent

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

English

For any polynomial f ∈ R[X], trunc(toLaurent f) = f.

Русский

Для любого полинома f ∈ R[X], trunc(toLaurent f) = f.

LaTeX

$$$\forall f \in R[X],\ trunc(toLaurent f) = f$$$

Lean4

@[simp]
theorem _root_.Polynomial.trunc_toLaurent (f : R[X]) : trunc (toLaurent f) = f :=
  leftInverse_trunc_toLaurent _

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

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

Разделы

Аффилиация

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