derivativeFinsupp_C — Mathlib

English

For any ring R and r ∈ R, the image of the constant polynomial C r under derivativeFinsupp is the finitely supported function with a single nonzero entry at 0 equal to C r.

Русский

Для любого кольца R и r ∈ R образ константного полинома C r под derivativeFinsupp равен конечной опоре с единственным ненулевым элементом в позиции 0 равным C r.

LaTeX

$$$$ \mathrm{derivativeFinsupp}(\,C(r)\,)=\mathrm{single}(0, C(r)) $$$$

Lean4

@[simp]
theorem derivativeFinsupp_C (r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r) :=
  by
  ext i : 1
  match i with
  | 0 => simp
  | i + 1 => simp

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