mkDerivation_X

Mathlib.Algebra.MvPolynomial.Derivation

URI: https://scilib.ai/kg/mathlib#MvPolynomial.mkDerivation_X

English

MkDerivation_X states the action of mkDerivation on X_i equals f(i).

Русский

MkDerivation_X задаёт, что mkDerivation на X_i равно f(i).

LaTeX

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

Lean4

@[simp]
theorem mkDerivation_X (f : σ → A) (i : σ) : mkDerivation R f (X i) = f i :=
  mkDerivationₗ_X f i

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

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

Разделы

Аффилиация

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