mkDerivation — Mathlib

English

For every a and f, mkDerivation R a f equals derivative f multiplied by a; this is a reiteration.

Русский

Для любого a и f, mkDerivation R a f равно производной f, умноженной на a; повторение.

LaTeX

$$$mkDerivation\ R\ a\ f = (\mathrm{derivative}\; f) \cdot a$$$

Lean4

/-- The derivation on `R[X]` that takes the value `a` on `X`. -/
def mkDerivation : A →ₗ[R] Derivation R R[X] A
    where
  toFun := fun a ↦ (LinearMap.toSpanSingleton R[X] A a).compDer derivative'
  map_add' := fun a b ↦ by ext; simp
  map_smul' := fun t a ↦ by ext; simp

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