algebraMap_eq_toLaurent — Mathlib

English

For every polynomial f in R[X], the image under the algebra map to Laurent polynomials equals toLaurent(f).

Русский

Для каждого многочлена f ∈ R[X] образ под отображением алгебры в лаурентовы полиномы равен toLaurent(f).

LaTeX

$$$\\mathrm{algebraMap}_{R[X] \\to \\mathrm{LaurentPolynomial}(R)}(f) = \\mathrm{toLaurent}(f).$$$

Lean4

@[simp]
theorem algebraMap_eq_toLaurent (f : R[X]) : algebraMap R[X] R[T;T⁻¹] f = toLaurent f :=
  rfl

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