cotangentComplex_mk — Mathlib

English

On a generator x, cotangentComplex evaluates to the basic tensor 1 ⊗ D x, i.e., the derivation applied to x inserted into the tensor product.

Русский

На генераторе x выражение cotangentComplex(x) равно базовой тензорной форме 1 ⊗ D x, то есть применённая выводная операция D к x внутри тензорного произведения.

LaTeX

$$\\cotangentComplex(\\mathrm{mk}(x)) = 1 \\otimes \\mathrm{D} x$$

Lean4

@[simp]
theorem cotangentComplex_mk (x) : P.cotangentComplex (.mk x) = 1 ⊗ₜ .D _ _ x :=
  rfl

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