coeff_derivativeFun — Mathlib

English

If every coefficient of f lies in I, then every coefficient of f·g lies in I, assuming I is a two-sided ideal.

Русский

Если каждый коэффициент f принадлежит I, то каждый коэффициент (f·g) принадлежит I, при условии, что I — двусторонний идеал.

LaTeX

$$$ (\\forall i, \\operatorname{coeff}_i f \\in I) \\Rightarrow (\\forall i, \\operatorname{coeff}_i(f g) \\in I)$$$

Lean4

theorem coeff_derivativeFun (f : R⟦X⟧) (n : ℕ) : coeff n f.derivativeFun = coeff (n + 1) f * (n + 1) := by
  rw [derivativeFun, coeff_mk]

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