mkDerivationₗ_X

Mathlib.Algebra.MvPolynomial.Derivation

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

English

The derivation sends X_i to f(i).

Русский

Производная отправляет X_i в f(i).

LaTeX

$$$\\\\mathrm{mkDerivation}_{\\ell}(R,f)(X_i) = f(i)$$$

Lean4

theorem mkDerivationₗ_X (f : σ → A) (i : σ) : mkDerivationₗ R f (X i) = f i :=
  (mkDerivationₗ_monomial f _ _).trans <| by simp [tsub_self]

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

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

Разделы

Аффилиация

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