derivativeFinsupp_X — Mathlib

English

The derivativeFinsupp of the indeterminate X in R[X] is the sum of two basis derivatives: derivativeFinsupp(X) = single 0 X + single 1 1.

Русский

ПроизводнаяFinsupp для X в R[X] равна сумме двух базисных производных: derivativeFinsupp(X) = single 0 X + single 1 1.

LaTeX

$$$$ \mathrm{derivativeFinsupp}(X) = \mathrm{single}(0, X) + \mathrm{single}(1, 1) $$$$

Lean4

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

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