English
Let R be a commutative semiring. The constant Laurent polynomial C r coincides with the image of r under the canonical algebra map from R to the Laurent polynomial ring R[T; T^{-1}].
Русский
Пусть R — коммутативное полугруппа с единицей; постоянный лаурентовский многочлен C r совпадает с образом r через каноническое алгебраическое отображение R → R[T; T^{-1}].
LaTeX
$$$ C r = \\operatorname{algebraMap} R R[T;T^{-1}]\\, r $$$
Lean4
/-- When we have `[CommSemiring R]`, the function `C` is the same as `algebraMap R R[T;T⁻¹]`.
(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebraMap` is not available.)
-/
theorem C_eq_algebraMap {R : Type*} [CommSemiring R] (r : R) : C r = algebraMap R R[T;T⁻¹] r :=
rfl
