DLinearMap_apply — Mathlib

English

The linear map KaehlerDifferential.DLinearMap sends s to the cotangent class of 1 ⊗ s − s ⊗ 1.

Русский

Линейное отображение DLinearMap отправляет s к классу котангента 1 ⊗ s − s ⊗ 1.

LaTeX

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

Lean4

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

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