mvPolynomialBasis_apply

Mathlib.RingTheory.Kaehler.Polynomial

URI: https://scilib.ai/kg/mathlib#KaehlerDifferential.mvPolynomialBasis_apply

← MathLib Explorer

English

The basis element indexed by i equals D_R(MvPolynomial(σ,R))(X_i).

Русский

Элемент базиса с индексом i равен D_R(MvPolynomial)(X_i).

LaTeX

$$$\\text{mvPolynomialBasis } R\\; σ\\; i = D\\, R\\, (MvPolynomial\\; σ\\; R)\\; (X_i).$$$

Lean4

@[simp]
theorem mvPolynomialBasis_apply (σ) (i) : mvPolynomialBasis R σ i = D R (MvPolynomial σ R) (.X i) :=
  (mvPolynomialBasis_repr_symm_single R σ i 1).trans (one_smul _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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