D_apply — Mathlib

English

The differential D evaluated via toCotangent coincides with the Cotangent representation.

Русский

Дифференциал, вычисляемый через toCotangent, совпадает с котангентной формой.

LaTeX

$$D_apply (s) = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ s - s ⊗ₜ 1, ...⟩$$

Lean4

theorem D_apply (s : S) :
    KaehlerDifferential.D R S s =
      (KaehlerDifferential.ideal R S).toCotangent
        ⟨1 ⊗ₜ s - s ⊗ₜ 1, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R s⟩ :=
  rfl

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