Theorems · Theorem · functional analysis

LineDeriv.iteratedLineDerivOp_neg

∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup E] [LineDerivAdd V E E] (x : E),
  LineDeriv.iteratedLineDerivOp m (-x) = -LineDeriv.iteratedLineDerivOp m x

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

LineDerivAddCommGroupAddCommGroupLineDerivAdd