Theorems · Theorem · functional analysis

LineDerivAdd.lineDerivOp_left_add

∀ {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : AddCommGroup V} {inst_1 : AddCommGroup E}
  {inst_2 : AddCommGroup F} {inst_3 : LineDeriv V E F} [self : LineDerivAdd V E F] (v w : V) (x : E),
  LineDeriv.lineDerivOp (v + w) x = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp w x

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

3 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

LineDerivAdd