Theorems · Theorem · functional analysis

LineDeriv.iteratedLineDerivOp_smul

∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : SMul R E]
  [LineDerivSMul R V E E] (r : R) (x : E),
  LineDeriv.iteratedLineDerivOp m (r • x) = r • LineDeriv.iteratedLineDerivOp m x

Defined in: Mathlib.Analysis.Distribution.DerivNotation
Cited by: 0 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext
Assumes: LineDeriv SMul LineDerivSMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fin.tailproof · cited by 74
LineDeriv.lineDerivOpproof · cited by 60
LineDerivstatement and proof · cited by 29
LineDeriv.iteratedLineDerivOpstatement and proof · cited by 18
LineDerivSMulstatement and proof · cited by 9
LineDerivSMul.lineDerivOp_smulproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.