cotangentSpaceBasis_repr_tmul — Mathlib

English

For i, the basis element P.cotangentSpaceBasis.repr applied to (r ⊗ KaehlerDifferential.D x) at i equals r times the evaluation of the derivative pderiv i on x.

Русский

Для индекса i элемент базиса P.cotangentSpaceBasis.repr применённый к (r ⊗ D x) в позиции i равен r умножить на eval(pderiv i) по x.

LaTeX

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

Lean4

@[simp]
theorem cotangentSpaceBasis_repr_tmul (r x i) :
    P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] KaehlerDifferential.D R P.Ring x : _) i = r * aeval P.val (pderiv i x) :=
  by
  classical
    simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply, Algebra.smul_def,
    mul_comm r, algebraMap_apply, toExtension]

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