δAux_X

Mathlib.RingTheory.Kaehler.JacobiZariski

URI: https://scilib.ai/kg/mathlib#Algebra.Generators.H1Cotangent.δAux_X

English

The auxiliary map δAux evaluates to zero on the simple X_i generators: δAux(R,Q)(X_i) = 0 for all i.

Русский

δAux(R,Q) обнуляется на базисных генераторах X_i: δAux(R,Q)(X_i) = 0 для всех i.

LaTeX

$$$$ \forall i, \deltaAux\,R\,Q (X_i) = 0. $$$$

Lean4

@[simp]
theorem δAux_X (i) : δAux R Q (X i) = 0 := by
  rw [X, δAux_monomial]
  simp only [Derivation.map_one_eq_zero, tmul_zero]

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

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

Разделы

Аффилиация

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