single_eq_C — Mathlib

English

In the Laurent polynomial ring, the Finsupp representation with only exponent 0 and value r equals the constant Laurent polynomial C r.

Русский

В кольце лаурентовских многочленов представление Finsupp, состоящее только из степени 0 и значения r, равно константному лаурентовскому многочлену C r.

LaTeX

$$$Finsupp.single 0\\, r = C\\, r$$$

Lean4

theorem single_eq_C (r : R) : Finsupp.single 0 r = C r :=
  rfl

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