comm₂₃' — Mathlib

English

A restatement of comm₂₃' in terms of the full differential framework, matching the explicit expression for the differential of the presentation relation.

Русский

Переформулировка comm₂₃' в рамках полной дифференциальной теории, сопоставляющая дифференциал презентирующего отношения.

LaTeX

$$$pres.toExtension.toKaehler.comp pres.cotangentSpaceBasis.repr.symm.toLinearMap = Finsupp.linearCombination S (\\lambda g \\, D _ _ (pres.val g))$$$

Lean4

/-- Same as `comm₂₃` below, but here we have not yet constructed `differentialsSolution`. -/
theorem comm₂₃' :
    pres.toExtension.toKaehler.comp pres.cotangentSpaceBasis.repr.symm.toLinearMap =
      Finsupp.linearCombination S (fun g ↦ D _ _ (pres.val g)) :=
  by
  ext
  simp

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