toLaurent_one — Mathlib

English

The Laurent embedding sends constant polynomials to constants: toLaurent(C r) = C r for all r ∈ R.

Русский

В лаурентовом вложении константные многочлены сохраняются: toLaurent(C r) = C r для всех $r\\in R$.

LaTeX

$$$\\forall r,\\; toLaurent (Polynomial.C\\, r) = C\\, r$$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_one : (Polynomial.toLaurent : R[X] → R[T;T⁻¹]) 1 = 1 :=
  map_one Polynomial.toLaurent

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