mapCoeffs_monomial — Mathlib

English

For any derivation d, the mapCoeffs of a monomial n-th degree with coefficient x is the polynomial with a single term at n having value d(x).

Русский

Для любой производной d mapCoeffs отображает мономиал n-ой степени с коэффициентом x в полином, содержащий единственный член при степени n и значением d(x).

LaTeX

$$$d.mapCoeffs(\mathrm{monomial}(n,x)) = \mathrm{single}^{A}_{n}(d(x)).$$$

Lean4

@[simp]
theorem mapCoeffs_monomial (n : ℕ) (x : A) : d.mapCoeffs (monomial n x) = .single A n (d x) :=
  Finsupp.ext fun _ ↦ by simp [coeff_monomial, apply_ite d, PolynomialModule.single_apply]

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