Theorems · Theorem · functional analysis

LineDeriv.iteratedLineDerivOpCLM_apply

∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] [inst_1 : TopologicalSpace E] [inst_2 : Ring R]
  [inst_3 : AddCommGroup V] [inst_4 : AddCommGroup E] [inst_5 : Module R E] [inst_6 : LineDerivAdd V E E]
  [inst_7 : LineDerivSMul R V E E] [inst_8 : ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) (x : E),
  (LineDeriv.iteratedLineDerivOpCLM R E m) x = LineDeriv.iteratedLineDerivOp m x

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext

Assumes

LineDerivTopologicalSpaceRingAddCommGroupAddCommGroupModuleLineDerivAddLineDerivSMulContinuousLineDeriv