toFinsupp_C_mul_X — Mathlib

English

Let a be an element of a semiring R. The polynomial C a · X has exactly one nonzero coefficient, at degree 1, equal to a.

Русский

Пусть a ∈ R. Полином C a · X имеет ровно один ненулевой коэффициент, при степени 1, равный a.

LaTeX

$$$\operatorname{coeff}(C a \cdot X, n) = \begin{cases} a & n=1 \\ 0 & n \neq 1 \end{cases}$$$

Lean4

@[simp high]
theorem toFinsupp_C_mul_X (a : R) : Polynomial.toFinsupp (C a * X) = Finsupp.single 1 a := by
  rw [C_mul_X_eq_monomial, toFinsupp_monomial]

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