basisDeriv_apply — Mathlib

English

The i-th basis element of basisDeriv equals the evaluation of the derivative of map j on relation i, via aeval.

Русский

i-ый элемент базиса basisDeriv равен вычислению производной отображения j на отношении i через aeval.

LaTeX

$$$\\text{basisDeriv}_i j = (\\mathrm{aeval}(P.val))\\big(\\mathrm{pderiv}(P.map(j))(P.relation(i))\\big)$$$

Lean4

@[simp]
theorem basisDeriv_apply (i j : σ) : P.basisDeriv i j = (aeval P.val) (pderiv (P.map j) (P.relation i)) := by
  classical simp [basisDeriv]

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