cotangentSpaceBasis_repr_one_tmul

English

When taking 1 ⊗ D x and evaluating at i, the representation equals the derivative evaluation without the r factor.

Русский

При взятии 1 ⊗ D x и рассмотрении на i, представление равно eval(pderiv i x) без множителя r.

LaTeX

$$$P.cotangentSpaceBasis.repr (TensorProduct.tmul P.Ring 1 (KaehlerDifferential.D R P.Ring x))\\!_i = aeval P.val (pderiv i x)$$$

Lean4

theorem cotangentSpaceBasis_repr_one_tmul (x i) :
    P.cotangentSpaceBasis.repr (1 ⊗ₜ .D _ _ x) i = aeval P.val (pderiv i x) := by simp

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