mkDerivationₗ_C

Mathlib.Algebra.MvPolynomial.Derivation

URI: https://scilib.ai/kg/mathlib#MvPolynomial.mkDerivationₗ_C

English

MkDerivation applied to constants yields zero; the derivation vanishes on constants.

Русский

Производная на константах равна нулю; производная обращается в ноль на константах.

LaTeX

$$$\\\\mathrm{mkDerivation}_{\\ell}(R,f)(C r) = 0$$$

Lean4

theorem mkDerivationₗ_C (f : σ → A) (r : R) : mkDerivationₗ R f (C r) = 0 :=
  (mkDerivationₗ_monomial f _ _).trans (smul_zero _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru